---

Step * of Lemma div_4_to_1

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

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

---

Latex:

---

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


By

---

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

---

Home Index