---

Step * of Lemma div_minus

∀[a:ℤ]. ∀[b:ℤ-o].  (((-a) ÷ -b) = (a ÷ b) ∈ ℤ)
BY
{ (Auto THEN (Assert -b ≠ 0 BY ((D 0 THENA Auto) THEN Add ⌜b⌝ (-1)⋅ THEN Auto))) }

1
1. a : ℤ
2. b : ℤ-o
3. -b ≠ 0
⊢ ((-a) ÷ -b) = (a ÷ b) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[b:\mBbbZ{}\msupminus{}\msupzero{}].    (((-a)  \mdiv{}  -b)  =  (a  \mdiv{}  b))


By

---

Latex:
(Auto  THEN  (Assert  -b  \mneq{}  0  BY  ((D  0  THENA  Auto)  THEN  Add  \mkleeneopen{}b\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)))

---

Home Index