Step 
*
 of Lemma 
fact_add1
∀[n:ℕ]. ((n + 1)! ~ (n + 1) * (n)!)
BY
 
{ Auto }
 
Latex: 
Latex:
\mforall{}[n:\mBbbN{}].  ((n  +  1)!  \msim{}  (n  +  1)  *  (n)!)
 By 
Latex:
Auto
Home
Index