---

Step * of Lemma triangular-num-add1

∀[n:ℕ]. (t(n + 1) = (t(n) + n + 1) ∈ ℤ)
BY
{ TACTIC:(TACTIC:Auto THEN Unfold `triangular-num` 0) }

1
1. n : ℕ
⊢ (((n + 1) * ((n + 1) + 1)) ÷ 2) = (((n * (n + 1)) ÷ 2) + n + 1) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (t(n  +  1)  =  (t(n)  +  n  +  1))


By

---

Latex:
TACTIC:(TACTIC:Auto  THEN  Unfold  `triangular-num`  0)

---

Home Index