---

Step * of Lemma exp-as-genfact

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

---

Latex:

---

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


By

---

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

---

Home Index