---

Step * of Lemma triangular-num-le

∀[n,m:ℕ].  t(n) ≤ t(m) supposing n ≤ m
BY
{ TACTIC:(TACTIC:Auto THEN Assert ⌜∀k:ℕ. (t(n) ≤ t(n + k))⌝⋅) }

1
.....assertion..... 
1. n : ℕ
2. m : ℕ
3. n ≤ m
⊢ ∀k:ℕ. (t(n) ≤ t(n + k))

2
1. n : ℕ
2. m : ℕ
3. n ≤ m
4. ∀k:ℕ. (t(n) ≤ t(n + k))
⊢ t(n) ≤ t(m)

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].    t(n)  \mleq{}  t(m)  supposing  n  \mleq{}  m


By

---

Latex:
TACTIC:(TACTIC:Auto  THEN  Assert  \mkleeneopen{}\mforall{}k:\mBbbN{}.  (t(n)  \mleq{}  t(n  +  k))\mkleeneclose{}\mcdot{})

---

Home Index