---

Step * 2 of Lemma triangular-num-le


1. n : ℕ
2. m : ℕ
3. n ≤ m
4. ∀k:ℕ. (t(n) ≤ t(n + k))
⊢ t(n) ≤ t(m)
BY
{ ((InstHyp [⌜m - n⌝] (-1)⋅ THEN Auto) THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  n  \mleq{}  m
4.  \mforall{}k:\mBbbN{}.  (t(n)  \mleq{}  t(n  +  k))
\mvdash{}  t(n)  \mleq{}  t(m)


By

---

Latex:
((InstHyp  [\mkleeneopen{}m  -  n\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)  THEN  Auto')

---

Home Index