---

Step * of Lemma fact_add2

∀[n:ℕ]. ((n + 2)! ~ (n + 2) * (n + 1) * (n)!)
BY
{ (Auto THEN (Subst' n + 2 ~ (n + 1) + 1 0 THENA Auto) THEN RWW "fact_add1" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  ((n  +  2)!  \msim{}  (n  +  2)  *  (n  +  1)  *  (n)!)


By

---

Latex:
(Auto  THEN  (Subst'  n  +  2  \msim{}  (n  +  1)  +  1  0  THENA  Auto)  THEN  RWW  "fact\_add1"  0  THEN  Auto)

---

Home Index