---

Step * 1 of Lemma zero-div-rem


1. x : ℤ-o
⊢ |0| < |x|
BY
{ TACTIC:(Subst' |0| ~ 0 0 THENA Auto) }

1
1. x : ℤ-o
⊢ 0 < |x|

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}\msupminus{}\msupzero{}
\mvdash{}  |0|  <  |x|


By

---

Latex:
TACTIC:(Subst'  |0|  \msim{}  0  0  THENA  Auto)

---

Home Index