---

Step * of Lemma nat-pred-as-sub

∀n:ℕ. (0 < n ⇒ (n-1 = (n - 1) ∈ ℕ))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``nat-pred`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (0  <  n  {}\mRightarrow{}  (n-1  =  (n  -  1)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``nat-pred``  0  THEN  AutoSplit)

---

Home Index