rewrite < Zplus_z_OZ.
rewrite < (Zplus_z_OZ y).
rewrite < (Zplus_Zopp x).
-rewrite < (Zplus_Zopp x).
rewrite < assoc_Zplus.
rewrite < assoc_Zplus.
apply eq_f2
[apply (bool_elim ? (leb ((S n1)*(S n1)) m))
[intro;rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? % ?))
[rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %))
- [rewrite > H1;rewrite > H2;rewrite < assoc_times;reflexivity
+ [rewrite > H1;rewrite < assoc_times;reflexivity
|rewrite > H;lapply (leb_true_to_le ? ? H2);
lapply (le_to_not_lt ? ? Hletin);
apply (bool_elim ? (leb (S m) (S n1 * S n1)))
sigma (S (p+n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m.
intros. elim p.
simplify.
-rewrite < (sym_plus n m).reflexivity.
+reflexivity.
simplify.
rewrite > assoc_plus in \vdash (? ? ? %).
rewrite < H.
apply H5
[rewrite < H8.assumption
|apply le_n
- |unfold.intro.rewrite > H8 in H2.
+ |unfold.intro.
apply (not_le_Sn_n n).rewrite < H9.assumption
]
]
|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) =