---

Step * of Lemma divides_instance

3 | 6
BY
{ (Assert ⌜TERMOF{decidable__divides_ext:o, \\v:l} 3 6 ∈ Dec(3 | 6)⌝⋅ THENA Auto{1,3}-1) }

1
1. TERMOF{decidable__divides_ext:o, \\v:l} 3 6 ∈ Dec(3 | 6)
⊢ 3 | 6

---

Latex:

---

Latex:
3  |  6


By

---

Latex:
(Assert  \mkleeneopen{}TERMOF\{decidable\_\_divides\_ext:o,  \mbackslash{}\mbackslash{}v:l\}  3  6  \mmember{}  Dec(3  |  6)\mkleeneclose{}\mcdot{}  THENA  Auto\{1,3\}-1)

---

Home Index