---

Step * of Lemma div_2_to_1

∀[a:{...0}]. ∀[b:ℕ+].  ((a ÷ b) = (-((-a) ÷ b)) ∈ ℤ)
BY
{ (Auto THEN (D 2 THENA Auto) THEN (D 1 THENA Auto) THEN Add ⌜-a⌝ 2⋅ THEN (RW  IntNormC (-1) THENA Auto)) }

1
1. a : ℤ
2. a ≤ 0
3. b : ℤ
4. 0 < b
5. 0 ≤ ((-1) * a)
⊢ (a ÷ b) = (-((-a) ÷ b)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[a:\{...0\}].  \mforall{}[b:\mBbbN{}\msupplus{}].    ((a  \mdiv{}  b)  =  (-((-a)  \mdiv{}  b)))


By

---

Latex:
(Auto
  THEN  (D  2  THENA  Auto)
  THEN  (D  1  THENA  Auto)
  THEN  Add  \mkleeneopen{}-a\mkleeneclose{}  2\mcdot{}
  THEN  (RW    IntNormC  (-1)  THENA  Auto))

---

Home Index