---

Step * of Lemma div_anti_sym

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

1
.....assertion..... 
1. a : ℤ
2. b : ℤ-o
⊢ -b ≠ 0

2
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  \mkleeneopen{}-b  \mneq{}  0\mkleeneclose{}\mcdot{})

---

Home Index