---

Step * of Lemma zero-div-rem

∀[x:ℤ-o]. ((0 ÷ x ~ 0) ∧ (0 rem x ~ 0))
BY
{ (Auto THEN Try (((BLemma `div_unique3` THEN Auto) THEN With ⌜0⌝ (D 0)⋅ THEN Auto))) }

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

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}\msupminus{}\msupzero{}].  ((0  \mdiv{}  x  \msim{}  0)  \mwedge{}  (0  rem  x  \msim{}  0))


By

---

Latex:
(Auto  THEN  Try  (((BLemma  `div\_unique3`  THEN  Auto)  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))

---

Home Index