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