---

Step * of Lemma subtract_nat_wf

∀[i,j:ℤ].  i - j ∈ ℕ supposing j ≤ i
BY
{ TACTIC:Auto' }

---

Latex:

---

Latex:
\mforall{}[i,j:\mBbbZ{}].    i  -  j  \mmember{}  \mBbbN{}  supposing  j  \mleq{}  i


By

---

Latex:
TACTIC:Auto'

---

Home Index