---

Step * of Lemma fact_unroll_1

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

---

Latex:

---

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


By

---

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

---

Home Index