|apply le_log
[assumption
|cut (O = exp O n!)
- [rewrite > Hcut;apply monotonic_exp1;constructor 2;
+ [apply monotonic_exp1;constructor 2;
apply leb_true_to_le;assumption
|elim n
[reflexivity
|assumption]
|assumption]
|assumption]
- |do 2 rewrite > false_to_sigma_p_Sn;assumption]]
+ |do 2 try rewrite > false_to_sigma_p_Sn;assumption]]
qed.
lemma neper_sigma_p3 : \forall a,n.O < a \to O < n \to n \divides a \to (exp (S n) n)/(exp n n) =