---

Step * of Lemma decidable__divides

∀a,b:ℤ.  Dec(a | b)
BY
{ (Auto THEN (Decide ⌜a = 0 ∈ ℤ⌝ THENA Auto)) }

1
1. a : ℤ
2. b : ℤ
3. a = 0 ∈ ℤ
⊢ Dec(a | b)

2
1. a : ℤ
2. b : ℤ
3. ¬(a = 0 ∈ ℤ)
⊢ Dec(a | b)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    Dec(a  |  b)


By

---

Latex:
(Auto  THEN  (Decide  \mkleeneopen{}a  =  0\mkleeneclose{}  THENA  Auto))

---

Home Index