---

Step * of Lemma fact_unroll_1

∀[n:ℤ]. (n)! ~ n * (n - 1)! supposing ¬n < 1
BY
{ xxx(RepeatFor 2 ((D 0 THENA Auto)) THEN (RW (AddrC [1] (LemmaC `fact_unroll`)) 0 THENA Auto) THEN AutoSplit)xxx }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  (n)!  \msim{}  n  *  (n  -  1)!  supposing  \mneg{}n  <  1


By

---

Latex:
xxx(RepeatFor  2  ((D  0  THENA  Auto))
        THEN  (RW  (AddrC  [1]  (LemmaC  `fact\_unroll`))  0  THENA  Auto)
        THEN  AutoSplit)xxx

---

Home Index