include "nat/iteration2.ma".
include "nat/div_and_mod_diseq.ma".
+include "nat/binomial.ma".
-theorem boh: \forall n,m.
+theorem sigma_p_div_exp: \forall n,m.
sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le
((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
intros.
]
]
qed.
-
\ No newline at end of file
+
+theorem le_fact_exp: \forall i,m. i \le m \to m!≤ m \sup i*(m-i)!.
+intro.elim i
+ [rewrite < minus_n_O.
+ simplify.rewrite < plus_n_O.
+ apply le_n
+ |simplify.
+ apply (trans_le ? ((m)\sup(n)*(m-n)!))
+ [apply H.
+ apply lt_to_le.assumption
+ |rewrite > sym_times in ⊢ (? ? (? % ?)).
+ rewrite > assoc_times.
+ apply le_times_r.
+ generalize in match H1.
+ cases m;intro
+ [apply False_ind.
+ apply (lt_to_not_le ? ? H2).
+ apply le_O_n
+ |rewrite > minus_Sn_m.
+ simplify.
+ apply le_plus_r.
+ apply le_times_l.
+ apply le_minus_m.
+ apply le_S_S_to_le.
+ assumption
+ ]
+ ]
+ ]
+qed.
+
+theorem le_fact_exp1: \forall n. S O < n \to (S(S O))*n!≤ n \sup n.
+intros.elim H
+ [apply le_n
+ |change with ((S(S O))*((S n1)*(fact n1)) \le (S n1)*(exp (S n1) n1)).
+ rewrite < assoc_times.
+ rewrite < sym_times in ⊢ (? (? % ?) ?).
+ rewrite > assoc_times.
+ apply le_times_r.
+ apply (trans_le ? (exp n1 n1))
+ [assumption
+ |apply monotonic_exp1.
+ apply le_n_Sn
+ ]
+ ]
+qed.
+
+theorem le_exp_sigma_p_exp: \forall n. (exp (S n) n) \le
+sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
+intro.
+rewrite > exp_S_sigma_p.
+apply le_sigma_p.
+intros.unfold bc.
+apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
+ [rewrite > sym_times.
+ apply le_times_r.
+ rewrite > sym_times.
+ rewrite < eq_div_div_div_times
+ [apply monotonic_div
+ [apply lt_O_fact
+ |apply le_times_to_le_div2
+ [apply lt_O_fact
+ |apply le_fact_exp.
+ apply le_S_S_to_le.
+ assumption
+ ]
+ ]
+ |apply lt_O_fact
+ |apply lt_O_fact
+ ]
+ |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
+ [rewrite > exp_plus_times.
+ apply le_times_div_div_times.
+ apply lt_O_fact
+ |apply le_S_S_to_le.
+ assumption
+ ]
+ ]
+qed.
+
+theorem lt_exp_sigma_p_exp: \forall n. S O < n \to
+(exp (S n) n) <
+sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
+intros.
+rewrite > exp_S_sigma_p.
+apply lt_sigma_p
+ [intros.unfold bc.
+ apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
+ [rewrite > sym_times.
+ apply le_times_r.
+ rewrite > sym_times.
+ rewrite < eq_div_div_div_times
+ [apply monotonic_div
+ [apply lt_O_fact
+ |apply le_times_to_le_div2
+ [apply lt_O_fact
+ |apply le_fact_exp.
+ apply le_S_S_to_le.
+ assumption
+ ]
+ ]
+ |apply lt_O_fact
+ |apply lt_O_fact
+ ]
+ |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
+ [rewrite > exp_plus_times.
+ apply le_times_div_div_times.
+ apply lt_O_fact
+ |apply le_S_S_to_le.
+ assumption
+ ]
+ ]
+ |apply (ex_intro ? ? n).
+ split
+ [split
+ [apply le_n
+ |reflexivity
+ ]
+ |rewrite < minus_n_n.
+ rewrite > bc_n_n.
+ simplify.unfold lt.
+ apply le_times_to_le_div
+ [apply lt_O_fact
+ |rewrite > sym_times.
+ apply le_fact_exp1.
+ assumption
+ ]
+ ]
+ ]
+qed.
+
+
+
+
+