---

Step * 1 of Lemma nat2inf_wf


1. n : ℕ
2. n@0 : ℕ@i
3. ↑n@0 + 1 <z n@i
⊢ n@0 < n
BY
{ (RW assert_pushdownC (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  n@0  :  \mBbbN{}@i
3.  \muparrow{}n@0  +  1  <z  n@i
\mvdash{}  n@0  <  n


By

---

Latex:
(RW  assert\_pushdownC  (-1)  THEN  Auto)

---

Home Index