---

Step * 2 of Lemma ni-min-nat


1. n : ℕ
2. m : ℕ
3. n@0 : ℕ
4. ↑(ni-min(n∞;m∞) (n@0 + 1))
⊢ ↑(ni-min(n∞;m∞) n@0)
BY
{ (RenameVar `i' (-2) THEN RepUR ``ni-min nat2inf`` -1 THEN RepUR ``ni-min nat2inf`` 0) }

1
1. n : ℕ
2. m : ℕ
3. i : ℕ
4. ↑(i + 1 <z n ∧b i + 1 <z m)
⊢ ↑(i <z n ∧b i <z m)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  n@0  :  \mBbbN{}
4.  \muparrow{}(ni-min(n\minfty{};m\minfty{})  (n@0  +  1))
\mvdash{}  \muparrow{}(ni-min(n\minfty{};m\minfty{})  n@0)


By

---

Latex:
(RenameVar  `i'  (-2)  THEN  RepUR  ``ni-min  nat2inf``  -1  THEN  RepUR  ``ni-min  nat2inf``  0)

---

Home Index