---

Step * of Lemma fact-as-genfact

∀[n:ℕ]. ((n)! ~ genfact(n;1;m.m))
BY
{ ((InductionOnNat THENA Auto) THENL [Computation; (RWO "fact_unroll genfact-step" 0 THEN Auto)]) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  ((n)!  \msim{}  genfact(n;1;m.m))


By

---

Latex:
((InductionOnNat  THENA  Auto)  THENL  [Computation;  (RWO  "fact\_unroll  genfact-step"  0  THEN  Auto)])

---

Home Index