---

Step * 2 1 of Lemma ni-min-nat


1. n : ℕ
2. m : ℕ
3. i : ℕ
4. ↑(i + 1 <z n ∧b i + 1 <z m)
⊢ ↑(i <z n ∧b i <z m)
BY
{ ((All (RW assert_pushdownC) THENA Auto) THEN ParallelLast THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  i  :  \mBbbN{}
4.  \muparrow{}(i  +  1  <z  n  \mwedge{}\msubb{}  i  +  1  <z  m)
\mvdash{}  \muparrow{}(i  <z  n  \mwedge{}\msubb{}  i  <z  m)


By

---

Latex:
((All  (RW  assert\_pushdownC)  THENA  Auto)  THEN  ParallelLast  THEN  Auto)

---

Home Index