---

Step * 1 of Lemma int-rinv-cancel2

.....rewrite subgoal..... 
1. a : ℤ
2. b : ℤ-o
⊢ rnonzero(r(b))
BY
{ EAuto 2 }

---

Latex:

---

Latex:
.....rewrite  subgoal..... 
1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}\msupminus{}\msupzero{}
\mvdash{}  rnonzero(r(b))


By

---

Latex:
EAuto  2

---

Home Index