---

Step * 1 of Lemma divides_reflexivity


1. a : ℤ
⊢ a | a
BY
{ Unfold `divides` 0 }

1
1. a : ℤ
⊢ ∃c:ℤ. (a = (a * c) ∈ ℤ)

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
\mvdash{}  a  |  a


By

---

Latex:
Unfold  `divides`  0

---

Home Index