]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/neper.ma
apply rule (lem EM) works
[helm.git] / helm / software / matita / library / nat / neper.ma
1 (**************************************************************************)
2 (*       __                                                               *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/iteration2.ma".
16 include "nat/div_and_mod_diseq.ma".
17 include "nat/binomial.ma".
18 include "nat/log.ma".
19 include "nat/chebyshev.ma".
20                   
21 theorem sigma_p_div_exp: \forall n,m.
22 sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le 
23 ((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
24 intros.
25 elim n
26   [apply le_O_n.
27   |rewrite > true_to_sigma_p_Sn
28     [apply (trans_le ? (m/(S(S O))\sup(n1)+((S(S O))*m*(S(S O))\sup(n1)-(S(S O))*m)/(S(S O))\sup(n1)))
29       [apply le_plus_r.assumption
30       |rewrite > assoc_times in ⊢ (? ? (? (? % ?) ?)).
31        rewrite < distr_times_minus.
32        change in ⊢ (? ? (? ? %)) with ((S(S O))*(exp (S(S O)) n1)).
33        rewrite > sym_times in ⊢ (? ? (? % ?)).
34        rewrite > sym_times in ⊢ (? ? (? ? %)).
35        rewrite < lt_to_lt_to_eq_div_div_times_times
36         [apply (trans_le ? ((m+((S(S O))*m*((S(S O)))\sup(n1)-(S(S O))*m))/((S(S O)))\sup(n1)))
37           [apply le_plus_div.
38            apply lt_O_exp.
39            apply lt_O_S
40           |change in ⊢ (? (? (? ? (? ? %)) ?) ?) with (m + (m +O)).
41            rewrite < plus_n_O.
42            rewrite < eq_minus_minus_minus_plus.
43            rewrite > sym_plus.
44            rewrite > sym_times in ⊢ (? (? (? (? (? (? % ?) ?) ?) ?) ?) ?).
45            rewrite > assoc_times.
46            rewrite < plus_minus_m_m
47             [apply le_n
48             |apply le_plus_to_minus_r.
49              rewrite > plus_n_O in ⊢ (? (? ? %) ?).
50              change in ⊢ (? % ?) with ((S(S O))*m). 
51              rewrite > sym_times.
52              apply le_times_r.
53              rewrite > times_n_SO in ⊢ (? % ?).
54              apply le_times_r.
55              apply lt_O_exp.
56              apply lt_O_S
57             ]
58           ]
59         |apply lt_O_S
60         |apply lt_O_exp.
61          apply lt_O_S
62         ]
63       ]
64     |reflexivity
65     ]
66   ]
67 qed.
68    
69 theorem le_fact_exp: \forall i,m. i \le m \to m!≤ m \sup i*(m-i)!.
70 intro.elim i
71   [rewrite < minus_n_O.
72    simplify.rewrite < plus_n_O.
73    apply le_n
74   |simplify.
75    apply (trans_le ? ((m)\sup(n)*(m-n)!))
76     [apply H.
77      apply lt_to_le.assumption
78     |rewrite > sym_times in ⊢ (? ? (? % ?)).
79      rewrite > assoc_times.
80      apply le_times_r.
81      generalize in match H1.
82      cases m;intro
83       [apply False_ind.
84        apply (lt_to_not_le ? ? H2).
85        apply le_O_n
86       |rewrite > minus_Sn_m.
87        simplify.
88        apply le_plus_r.
89        apply le_times_l.
90        apply le_minus_m.
91        apply le_S_S_to_le.
92        assumption
93       ]
94     ]
95   ]
96 qed.
97
98 theorem le_fact_exp1: \forall n. S O < n \to (S(S O))*n!≤ n \sup n.
99 intros.elim H
100   [apply le_n
101   |change with ((S(S O))*((S n1)*(fact n1)) \le (S n1)*(exp (S n1) n1)).   
102    rewrite < assoc_times.
103    rewrite < sym_times in ⊢ (? (? % ?) ?).
104    rewrite > assoc_times.
105    apply le_times_r.
106    apply (trans_le ? (exp n1 n1))
107     [assumption
108     |apply monotonic_exp1.
109      apply le_n_Sn
110     ]
111   ]
112 qed.
113    
114 theorem le_exp_sigma_p_exp: \forall n. (exp (S n) n) \le
115 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
116 intro.
117 rewrite > exp_S_sigma_p.
118 apply le_sigma_p.
119 intros.unfold bc.
120 apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
121   [rewrite > sym_times.
122    apply le_times_r.
123    rewrite > sym_times.
124    rewrite < eq_div_div_div_times
125     [apply monotonic_div
126       [apply lt_O_fact
127       |apply le_times_to_le_div2
128         [apply lt_O_fact
129         |apply le_fact_exp.
130          apply le_S_S_to_le.
131          assumption
132         ]
133       ]
134     |apply lt_O_fact
135     |apply lt_O_fact
136     ]
137   |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
138     [rewrite > exp_plus_times.
139      apply le_times_div_div_times.
140      apply lt_O_fact
141     |apply le_S_S_to_le.
142      assumption
143     ]
144   ]
145 qed.
146     
147 theorem lt_exp_sigma_p_exp: \forall n. S O < n \to
148 (exp (S n) n) <
149 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
150 intros.
151 rewrite > exp_S_sigma_p.
152 apply lt_sigma_p
153   [intros.unfold bc.
154    apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
155     [rewrite > sym_times.
156      apply le_times_r.
157      rewrite > sym_times.
158      rewrite < eq_div_div_div_times
159       [apply monotonic_div
160         [apply lt_O_fact
161         |apply le_times_to_le_div2
162           [apply lt_O_fact
163           |apply le_fact_exp.
164            apply le_S_S_to_le.
165            assumption
166           ]
167         ]
168       |apply lt_O_fact
169       |apply lt_O_fact
170       ]
171     |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
172       [rewrite > exp_plus_times.
173        apply le_times_div_div_times.
174        apply lt_O_fact
175       |apply le_S_S_to_le.
176        assumption
177       ]
178     ]
179   |apply (ex_intro ? ? n).
180    split
181     [split
182       [apply le_n
183       |reflexivity
184       ]
185     |rewrite < minus_n_n.
186      rewrite > bc_n_n.
187      simplify.unfold lt.
188      apply le_times_to_le_div
189       [apply lt_O_fact
190       |rewrite > sym_times.
191        apply le_fact_exp1.
192        assumption
193       ]
194     ]
195   ]
196 qed.
197
198 theorem le_exp_SSO_fact:\forall n. 
199 exp (S(S O)) (pred n) \le n!.
200 intro.elim n
201   [apply le_n
202   |change with ((S(S O))\sup n1 ≤(S n1)*n1!).
203    apply (nat_case1 n1);intros
204     [apply le_n
205     |change in ⊢ (? % ?) with ((S(S O))*exp (S(S O)) (pred (S m))).
206      apply le_times
207       [apply le_S_S.apply le_S_S.apply le_O_n
208       |rewrite < H1.assumption
209       ]
210     ]
211   ]
212 qed.
213        
214 theorem lt_SO_to_lt_exp_Sn_n_SSSO: \forall n. S O < n \to 
215 (exp (S n) n) < (S(S(S O)))*(exp n n).
216 intros.  
217 apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
218   [apply lt_exp_sigma_p_exp.assumption
219   |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
220     [apply le_sigma_p.intros.
221      apply le_times_to_le_div
222       [apply lt_O_exp.
223        apply lt_O_S
224       |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
225         [apply le_times_div_div_times.
226          apply lt_O_fact
227         |apply le_times_to_le_div2
228           [apply lt_O_fact
229           |rewrite < sym_times.
230            apply le_times_r.
231            apply le_exp_SSO_fact
232           ]
233         ]
234       ]
235     |rewrite > eq_sigma_p_pred
236       [rewrite > div_SO.
237        rewrite > sym_plus.
238        change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
239        apply le_plus_r.
240        apply (trans_le ? (((S(S O))*(exp n n)*(exp (S(S O)) n) - (S(S O))*(exp n n))/(exp (S(S O)) n)))
241         [apply sigma_p_div_exp
242         |apply le_times_to_le_div2
243           [apply lt_O_exp.
244            apply lt_O_S.
245           |apply le_minus_m
246           ]
247         ]
248       |reflexivity
249       ]
250     ]
251   ]
252 qed.     
253     
254 theorem lt_exp_Sn_n_SSSO: \forall n.
255 (exp (S n) n) < (S(S(S O)))*(exp n n).
256 intro.cases n;intros
257   [simplify.apply le_S.apply le_n
258   |cases n1;intros
259     [simplify.apply le_n
260     |apply lt_SO_to_lt_exp_Sn_n_SSSO.
261      apply le_S_S.apply le_S_S.apply le_O_n
262     ]
263   ]
264 qed.
265
266 theorem lt_exp_Sn_m_SSSO: \forall n,m. O < m \to
267 divides n m \to
268 (exp (S n) m) < (exp (S(S(S O))) (m/n)) *(exp n m).
269 intros.
270 elim H1.rewrite > H2.
271 rewrite < exp_exp_times.
272 rewrite < exp_exp_times.
273 rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?)).
274 rewrite > lt_O_to_div_times
275   [rewrite > times_exp.
276    apply lt_exp1
277     [apply (O_lt_times_to_O_lt ? n).
278      rewrite > sym_times.
279      rewrite < H2.
280      assumption
281     |apply lt_exp_Sn_n_SSSO
282     ]
283   |apply (O_lt_times_to_O_lt ? n1).
284    rewrite < H2.
285    assumption
286   ]
287 qed.
288
289 theorem le_log_exp_Sn_log_exp_n: \forall n,m,p. O < m \to S O < p \to
290 divides n m \to
291 log p (exp (S n) m) \le S((m/n)*S(log p (S(S(S O))))) + log p (exp n m).
292 intros.
293 apply (trans_le ? (log p (((S(S(S O))))\sup(m/n)*((n)\sup(m)))))
294   [apply le_log
295     [assumption
296     |apply lt_to_le.
297      apply lt_exp_Sn_m_SSSO;assumption
298     ]
299   |apply (trans_le ? (S(log p (exp (S(S(S O))) (m/n)) + log p (exp n m))))
300     [apply log_times.
301      assumption
302     |change in ⊢ (? ? %) with (S (m/n*S (log p (S(S(S O))))+log p ((n)\sup(m)))).
303      apply le_S_S.
304      apply le_plus_l.
305      apply log_exp1.
306      assumption
307     ]
308   ]
309 qed.
310
311 theorem le_log_exp_fact_sigma_p: \forall a,b,n,p. S O < p \to
312 O < a \to a \le b \to b \le n \to
313 log p (exp b n!) - log p (exp a n!) \le
314 sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))).
315 intros 7.
316 elim b
317   [simplify.
318    apply (lt_O_n_elim ? (lt_O_fact n)).intro.
319    apply le_n.
320   |apply (bool_elim ? (leb a n1));intro
321     [rewrite > true_to_sigma_p_Sn
322       [apply (trans_le ? (S (n!/n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(n!))-log p ((a)\sup(n!)))))
323         [rewrite > sym_plus. 
324          rewrite > plus_minus
325           [apply le_plus_to_minus_r.
326            rewrite < plus_minus_m_m
327             [rewrite > sym_plus.
328              apply le_log_exp_Sn_log_exp_n
329               [apply lt_O_fact
330               |assumption
331               |apply divides_fact;
332                  [apply (trans_le ? ? ? H1);apply leb_true_to_le;assumption
333                  |apply lt_to_le;assumption]]
334             |apply le_log
335               [assumption
336               |cut (O = exp O n!)
337                  [apply monotonic_exp1;constructor 2;
338                   apply leb_true_to_le;assumption
339                  |elim n
340                     [reflexivity
341                     |simplify;rewrite > exp_plus_times;rewrite < H6;
342                      rewrite > sym_times;rewrite < times_n_O;reflexivity]]]]
343         |apply le_log
344           [assumption
345           |apply monotonic_exp1;apply leb_true_to_le;assumption]]
346       |rewrite > sym_plus;rewrite > sym_plus in \vdash (? ? %);apply le_minus_to_plus;
347        rewrite < minus_plus_m_m;apply H3;apply lt_to_le;assumption]
348     |assumption]
349   |lapply (not_le_to_lt ? ? (leb_false_to_not_le ? ? H5));
350    rewrite > eq_minus_n_m_O
351     [apply le_O_n
352     |apply le_log
353        [assumption
354        |apply monotonic_exp1;assumption]]]]
355 qed.
356
357 theorem le_exp_div:\forall n,m,q. O < m \to 
358 exp (n/m) q \le (exp n q)/(exp m q).
359 intros.
360 apply le_times_to_le_div
361   [apply lt_O_exp.
362    assumption
363   |rewrite > times_exp.
364    rewrite < sym_times.
365    apply monotonic_exp1.
366    rewrite > (div_mod n m) in ⊢ (? ? %)
367     [apply le_plus_n_r
368     |assumption
369     ]
370   ]
371 qed.
372
373 theorem le_log_div_sigma_p: \forall a,b,n,p. S O < p \to
374 O < a \to a \le b \to b \le n \to
375 log p (b/a) \le
376 (sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))))/n!.
377 intros.
378 apply le_times_to_le_div
379   [apply lt_O_fact
380   |apply (trans_le ? (log p (exp (b/a) n!)))
381     [apply log_exp2
382       [assumption
383       |apply le_times_to_le_div
384         [assumption
385         |rewrite < times_n_SO.
386          assumption
387         ]
388       ]
389     |apply (trans_le ? (log p ((exp b n!)/(exp a n!)))) 
390       [apply le_log
391         [assumption
392         |apply le_exp_div.assumption
393         ]
394       |apply (trans_le ? (log p (exp b n!) - log p (exp a n!)))
395         [apply log_div
396           [assumption
397           |apply lt_O_exp.
398            assumption
399           |apply monotonic_exp1.
400            assumption
401           ]
402         |apply le_log_exp_fact_sigma_p;assumption
403         ]
404       ]
405     ]
406   ]
407 qed.
408       
409 theorem sigma_p_log_div1: \forall n,b. S O < b \to
410 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
411 \le sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n!
412 ).
413 intros.
414 apply le_sigma_p.intros.
415 apply le_log_div_sigma_p
416   [assumption
417   |apply prime_to_lt_O.
418    apply primeb_true_to_prime.
419    apply (andb_true_true ? ? H2)
420   |apply le_S_S_to_le.
421    assumption
422   |apply le_n
423   ]
424 qed.
425
426 theorem sigma_p_log_div2: \forall n,b. S O < b \to
427 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
428 \le 
429 (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!).
430 intros.
431 apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n!
432 )))
433   [apply sigma_p_log_div1.assumption
434   |apply le_times_to_le_div
435     [apply lt_O_fact
436     |rewrite > distributive_times_plus_sigma_p.
437      rewrite < sym_times in ⊢ (? ? %).
438      rewrite > distributive_times_plus_sigma_p.
439      apply le_sigma_p.intros.
440      apply (trans_le ? ((n!*(sigma_p n (λj:nat.leb i j) (λi:nat.S (n!/i*S (log b (S(S(S O)))))))/n!)))
441       [apply le_times_div_div_times.
442        apply lt_O_fact
443       |rewrite > sym_times.
444        rewrite > lt_O_to_div_times
445         [rewrite > distributive_times_plus_sigma_p.
446          apply le_sigma_p.intros.
447          rewrite < times_n_Sm in ⊢ (? ? %).
448          rewrite > plus_n_SO.
449          rewrite > sym_plus.
450          apply le_plus
451           [apply le_S_S.apply le_O_n
452           |rewrite < sym_times.
453            apply le_n
454           ]
455         |apply lt_O_fact
456         ]
457       ]
458     ]
459   ]
460 qed.
461
462 theorem sigma_p_log_div: \forall n,b. S O < b \to
463 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
464 \le (sigma_p n (\lambda i.leb (S n) (i*i)) (\lambda i.(prim i)*S(n!/i)))*S(log b (S(S(S O))))/n!
465 .
466 intros.
467 apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!))
468   [apply sigma_p_log_div2.assumption
469   |apply monotonic_div
470     [apply lt_O_fact
471     |apply le_times_l.
472      unfold prim.
473      cut
474      (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p))
475       (λp:nat.sigma_p n (λi:nat.leb p i) (λi:nat.S (n!/i)))
476      = sigma_p n (λi:nat.leb (S n) (i*i))
477        (λi:nat.sigma_p (S n) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i))))
478       [rewrite > Hcut.
479        apply le_sigma_p.intros.
480        rewrite < sym_times.
481        rewrite > distributive_times_plus_sigma_p.
482        rewrite < times_n_SO.
483        cut 
484         (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i))
485          = sigma_p (S i) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i)))
486         [rewrite > Hcut1.
487          apply le_sigma_p1.intros.
488          rewrite < andb_sym.
489          rewrite < andb_sym in ⊢ (? (? (? (? ? %)) ?) ?).
490          apply (bool_elim  ? (leb i1 i));intros
491           [apply (bool_elim  ? (leb (S n) (i1*i1)));intros
492             [apply le_n
493             |apply le_O_n
494             ]
495           |apply le_O_n
496           ]
497         |apply or_false_to_eq_sigma_p
498           [apply le_S.assumption
499           |intros.
500            left.rewrite > (lt_to_leb_false i1 i)
501             [rewrite > andb_sym.reflexivity
502             |assumption
503             ]
504           ]
505         ]
506       |apply sigma_p_sigma_p.intros.
507        apply (bool_elim ? (leb x y));intros
508         [apply (bool_elim ? (leb (S n) (x*x)));intros
509           [rewrite > le_to_leb_true in ⊢ (? ? ? (? % ?))
510             [reflexivity
511             |apply (trans_le ? (x*x))
512               [apply leb_true_to_le.assumption
513               |apply le_times;apply leb_true_to_le;assumption
514               ]
515             ]
516           |rewrite < andb_sym in ⊢ (? ? (? % ?) ?).
517            rewrite < andb_sym in ⊢ (? ? ? (? ? (? % ?))).
518            rewrite < andb_sym in ⊢ (? ? ? %).
519            reflexivity
520           ]
521         |rewrite < andb_sym.
522          rewrite > andb_assoc in ⊢ (? ? ? %).
523          rewrite < andb_sym in ⊢ (? ? ? (? % ?)).
524          reflexivity
525         ]
526       ]
527     ]
528   ]
529 qed.
530
531 theorem le_sigma_p_div_log_div_pred_log : \forall n,b,m. S O < b \to b*b \leq n \to
532 sigma_p (S n) (\lambda i.leb (S n) (i*i)) (\lambda i.m/(log b i))
533 \leq ((S (S O)) * n * m)/(pred (log b n)).
534 intros.
535 apply (trans_le ? (sigma_p (S n) 
536              (\lambda i.leb (S n) (i*i)) (\lambda i.(S (S O))*m/(pred (log b n)))))
537   [apply le_sigma_p;intros;apply le_times_to_le_div
538      [rewrite > minus_n_O in ⊢ (? ? (? %));rewrite < eq_minus_S_pred;
539       apply le_plus_to_minus_r;simplify;
540       rewrite < (eq_log_exp b ? H);
541       apply le_log;
542           [assumption
543           |simplify;rewrite < times_n_SO;assumption]
544      |apply (trans_le ? ((pred (log b n) * m)/log b i))
545         [apply le_times_div_div_times;apply lt_O_log
546           [elim (le_to_or_lt_eq ? ? (le_O_n i))
547             [assumption
548             |apply False_ind;apply not_eq_true_false;rewrite < H3;rewrite < H4;
549              reflexivity]
550           |apply (le_exp_to_le1 ? ? (S (S O)))
551             [apply lt_O_S;
552             |apply (trans_le ? (S n))
553                [apply le_S;simplify;rewrite < times_n_SO;assumption
554                |rewrite > exp_SSO;apply leb_true_to_le;assumption]]]
555         |apply le_times_to_le_div2
556           [apply lt_O_log
557             [elim (le_to_or_lt_eq ? ? (le_O_n i))
558               [assumption
559               |apply False_ind;apply not_eq_true_false;rewrite < H3;rewrite < H4;
560                reflexivity]
561           |apply (le_exp_to_le1 ? ? (S (S O)))
562             [apply lt_O_S;
563             |apply (trans_le ? (S n))
564                [apply le_S;simplify;rewrite < times_n_SO;assumption
565                |rewrite > exp_SSO;apply leb_true_to_le;assumption]]]
566           |rewrite > sym_times in \vdash (? ? %);rewrite < assoc_times;
567            apply le_times_l;rewrite > sym_times;
568            rewrite > minus_n_O in \vdash (? (? %) ?);
569            rewrite < eq_minus_S_pred;apply le_plus_to_minus;
570            simplify;rewrite < plus_n_O;apply (trans_le ? (log b (i*i)))
571              [apply le_log
572                 [assumption
573                 |apply lt_to_le;apply leb_true_to_le;assumption]
574              |rewrite > sym_plus;simplify;apply log_times;assumption]]]]
575         |rewrite > times_n_SO in \vdash (? (? ? ? (\lambda i:?.%)) ?);
576          rewrite < distributive_times_plus_sigma_p;
577          apply (trans_le ? ((((S (S O))*m)/(pred (log b n)))*n))
578            [apply le_times_r;apply (trans_le ? (sigma_p (S n) (\lambda i:nat.leb (S O) (i*i)) (\lambda Hbeta1:nat.S O)))
579              [apply le_sigma_p1;intros;do 2 rewrite < times_n_SO;
580               apply (bool_elim ? (leb (S n) (i*i)))
581                 [intro;cut (leb (S O) (i*i) = true)
582                   [rewrite > Hcut;apply le_n
583                   |apply le_to_leb_true;apply (trans_le ? (S n))
584                      [apply le_S_S;apply le_O_n
585                      |apply leb_true_to_le;assumption]]
586                 |intro;simplify in \vdash (? % ?);apply le_O_n]
587              |elim n
588                 [simplify;apply le_n
589                 |apply (bool_elim ? (leb (S O) ((S n1)*(S n1))));intro
590                    [rewrite > true_to_sigma_p_Sn
591                       [change in \vdash (? % ?) with (S (sigma_p (S n1) (\lambda i:nat.leb (S O) (i*i)) (\lambda Hbeta1:nat.S O)));
592                        apply le_S_S;assumption
593                       |assumption]
594                    |rewrite > false_to_sigma_p_Sn
595                       [apply le_S;assumption
596                       |assumption]]]]
597           |rewrite > sym_times in \vdash (? % ?);
598            rewrite > sym_times in \vdash (? ? (? (? % ?) ?));
599            rewrite > assoc_times;
600            apply le_times_div_div_times;
601            rewrite > minus_n_O in ⊢ (? ? (? %));rewrite < eq_minus_S_pred;
602            apply le_plus_to_minus_r;simplify;
603            rewrite < (eq_log_exp b ? H);
604            apply le_log;
605              [assumption
606              |simplify;rewrite < times_n_SO;assumption]]]
607 qed.
608
609 lemma neper_sigma_p1 : \forall n,a.n \divides a \to
610 exp (a * S n) n =
611 sigma_p (S n) (\lambda x.true) (\lambda k.(bc n k)*(exp n (n-k))*(exp a n)).
612 intros;rewrite < times_exp;rewrite > exp_S_sigma_p;
613 rewrite > distributive_times_plus_sigma_p;
614 apply eq_sigma_p;intros;
615   [reflexivity
616   |rewrite > sym_times;reflexivity;]
617 qed.
618
619 lemma eq_exp_pi_p : \forall a,n.(exp a n) = pi_p n (\lambda x.true) (\lambda x.a).
620 intros;elim n
621   [simplify;reflexivity
622   |change in \vdash (? ? % ?) with (a*exp a n1);rewrite > true_to_pi_p_Sn
623      [apply eq_f2
624         [reflexivity
625         |assumption]
626      |reflexivity]]
627 qed.
628
629 lemma eq_fact_pi_p : \forall n.n! = pi_p n (\lambda x.true) (\lambda x.S x).
630 intros;elim n
631   [simplify;reflexivity
632   |rewrite > true_to_pi_p_Sn
633      [change in \vdash (? ? % ?) with (S n1*n1!);apply eq_f2
634         [reflexivity
635         |assumption]
636      |reflexivity]]
637 qed.
638
639 lemma divides_pi_p : \forall m,n,p,f.m \leq n \to pi_p m p f \divides pi_p n p f.
640 intros;elim H
641   [apply divides_n_n
642   |apply (bool_elim ? (p n1));intro
643      [rewrite > true_to_pi_p_Sn
644         [rewrite > sym_times;rewrite > times_n_SO;apply divides_times
645            [assumption
646            |apply divides_SO_n]
647         |assumption]
648      |rewrite > false_to_pi_p_Sn;assumption]]
649 qed.
650
651 lemma divides_fact_fact : \forall m,n.m \leq n \to m! \divides n!.
652 intros;do 2 rewrite > eq_fact_pi_p;apply divides_pi_p;assumption.
653 qed.
654
655 lemma divides_times_to_eq : \forall a,b,c.O < c \to c \divides a \to a*b/c = a/c*b.
656 intros;elim H1;rewrite > H2;cases H;rewrite > assoc_times;do 2 rewrite > div_times;
657 reflexivity;
658 qed.
659
660 lemma divides_pi_p_to_eq : \forall k,p,f,g.(\forall x.p x = true \to O < g x \land (g x \divides f x)) \to
661 pi_p k p f/pi_p k p g = pi_p k p (\lambda x.(f x)/(g x)).
662 intros;
663 cut (\forall k1.(pi_p k1 p g \divides pi_p k1 p f))
664   [|intro;elim k1
665      [simplify;apply divides_n_n
666      |apply (bool_elim ? (p n));intro;
667         [rewrite > true_to_pi_p_Sn
668            [rewrite > true_to_pi_p_Sn
669               [elim (H n)
670                  [elim H4;elim H1;rewrite > H5;rewrite > H6;
671                   rewrite < assoc_times;rewrite > assoc_times in ⊢ (? ? (? % ?));
672                   rewrite > sym_times in ⊢ (? ? (? (? ? %) ?));
673                   rewrite > assoc_times;rewrite > assoc_times;
674                   apply divides_times
675                     [apply divides_n_n
676                     |rewrite > times_n_SO in \vdash (? % ?);apply divides_times
677                        [apply divides_n_n
678                        |apply divides_SO_n]]
679                  |assumption]
680               |assumption]
681            |assumption]
682         |rewrite > false_to_pi_p_Sn
683            [rewrite > false_to_pi_p_Sn
684               [assumption
685               |assumption]
686            |assumption]]]]
687 elim k
688   [simplify;reflexivity
689   |apply (bool_elim ? (p n))
690      [intro;rewrite > true_to_pi_p_Sn;
691         [rewrite > true_to_pi_p_Sn;
692            [rewrite > true_to_pi_p_Sn;
693               [elim (H n);
694                  [elim H4;rewrite > H5;rewrite < eq_div_div_div_times;
695                     [cases H3
696                        [rewrite > assoc_times;do 2 rewrite > div_times;
697                         elim (Hcut n);rewrite > H6;rewrite < assoc_times;
698                         rewrite < sym_times in \vdash (? ? (? (? % ?) ?) ?);
699                         cut (O < pi_p n p g)
700                           [rewrite < H1;rewrite > H6;cases Hcut1;
701                            rewrite > assoc_times;do 2 rewrite > div_times;reflexivity
702                           |elim n
703                              [simplify;apply le_n
704                              |apply (bool_elim ? (p n3));intro
705                                 [rewrite > true_to_pi_p_Sn
706                                    [rewrite > (times_n_O O);apply lt_times
707                                       [elim (H n3);assumption
708                                       |assumption]
709                                    |assumption]
710                                 |rewrite > false_to_pi_p_Sn;assumption]]]
711                        |rewrite > assoc_times;do 2 rewrite > div_times;
712                         elim (Hcut n);rewrite > H7;rewrite < assoc_times;
713                         rewrite < sym_times in \vdash (? ? (? (? % ?) ?) ?);
714                         cut (O < pi_p n p g)
715                           [rewrite < H1;rewrite > H7;cases Hcut1;
716                            rewrite > assoc_times;do 2 rewrite > div_times;reflexivity
717                           |elim n
718                              [simplify;apply le_n
719                              |apply (bool_elim ? (p n3));intro
720                                 [rewrite > true_to_pi_p_Sn
721                                    [rewrite > (times_n_O O);apply lt_times
722                                       [elim (H n3);assumption
723                                       |assumption]
724                                    |assumption]
725                                 |rewrite > false_to_pi_p_Sn;assumption]]]]
726                     |assumption
727                     |(*già usata 2 volte: fattorizzare*)
728                      elim n
729                        [simplify;apply le_n
730                        |apply (bool_elim ? (p n2));intro
731                           [rewrite > true_to_pi_p_Sn
732                              [rewrite > (times_n_O O);apply lt_times
733                                 [elim (H n2);assumption
734                                 |assumption]
735                              |assumption]
736                           |rewrite > false_to_pi_p_Sn;assumption]]]
737                  |assumption]
738               |assumption]
739            |assumption]
740         |assumption]
741      |intro;rewrite > (false_to_pi_p_Sn ? ? ? H2);
742       rewrite > (false_to_pi_p_Sn ? ? ? H2);rewrite > (false_to_pi_p_Sn ? ? ? H2);
743       assumption]]
744 qed.
745
746 lemma divides_times_to_divides_div : \forall a,b,c.O < b \to 
747                                     a*b \divides c \to a \divides c/b.
748 intros;elim H1;rewrite > H2;rewrite > sym_times in \vdash (? ? (? (? % ?) ?));
749 rewrite > assoc_times;cases H;rewrite > div_times;rewrite > times_n_SO in \vdash (? % ?);
750 apply divides_times
751   [1,3:apply divides_n_n
752   |*:apply divides_SO_n]
753 qed.
754
755 lemma neper_sigma_p2 : \forall n,a.O < n \to n \divides a \to
756 sigma_p (S n) (\lambda x.true) (\lambda k.((bc n k)*(exp a n)*(exp n (n-k)))/(exp n n))
757 = sigma_p (S n) (\lambda x.true) 
758 (\lambda k.(exp a (n-k))*(pi_p k (\lambda y.true) (\lambda i.a - (a*i/n)))/k!).
759 intros;apply eq_sigma_p;intros;
760   [reflexivity
761   |transitivity (bc n x*exp a n/exp n x)
762      [rewrite > minus_n_O in ⊢ (? ? (? ? (? ? %)) ?);
763       rewrite > (minus_n_n x);
764       rewrite < (eq_plus_minus_minus_minus n x x);
765         [rewrite > exp_plus_times;
766          rewrite > sym_times;rewrite > sym_times in \vdash (? ? (? ? %) ?);
767          rewrite < sym_times;
768          rewrite < sym_times in ⊢ (? ? (? ? %) ?);
769          rewrite < lt_to_lt_to_eq_div_div_times_times;
770            [reflexivity
771            |*:apply lt_O_exp;assumption]
772         |apply le_n
773         |apply le_S_S_to_le;assumption]
774      |rewrite > minus_n_O in ⊢ (? ? (? (? ? (? ? %)) ?) ?);
775       rewrite > (minus_n_n x);
776       rewrite < (eq_plus_minus_minus_minus n x x);
777         [rewrite > exp_plus_times;
778          unfold bc;
779          elim (bc2 n x)
780            [rewrite > H3;cut (x!*n1 = pi_p x (\lambda i.true) (\lambda i.(n - i)))
781               [rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
782                rewrite > assoc_times;
783                rewrite < sym_times in ⊢ (? ? (? (? (? % ?) ?) ?) ?);
784                rewrite < lt_to_lt_to_eq_div_div_times_times;
785                  [rewrite > Hcut;rewrite < assoc_times;
786                   cut (pi_p x (λi:nat.true) (λi:nat.n-i)/x!*(a)\sup(x)
787                     = pi_p x (λi:nat.true) (λi:nat.(n-i))*pi_p x (\lambda i.true) (\lambda i.a)/x!)
788                     [rewrite > Hcut1;rewrite < times_pi_p;
789                      rewrite > divides_times_to_eq in \vdash (? ? % ?);
790                        [rewrite > eq_div_div_div_times;
791                           [rewrite > sym_times in ⊢ (? ? (? (? ? %) ?) ?);
792                            rewrite < eq_div_div_div_times;
793                              [cut (exp n x = pi_p x (\lambda i.true) (\lambda i.n))
794                                 [rewrite > Hcut2;rewrite > divides_pi_p_to_eq
795                                    [rewrite > sym_times in \vdash (? ? ? %);
796                                     rewrite > divides_times_to_eq in \vdash (? ? ? %);
797                                       [apply eq_f2
798                                          [apply eq_f2
799                                             [apply eq_pi_p;intros
800                                                [reflexivity
801                                                |rewrite > sym_times;
802                                                 rewrite > distr_times_minus;elim H1;
803                                                 rewrite > H5;(* in ⊢ (? ? (? (? ? (? % ?)) ?) ?);*)
804                                                 rewrite > sym_times;rewrite > assoc_times;
805                                                 rewrite < distr_times_minus;
806                                                 generalize in match H;cases n;intros
807                                                   [elim (not_le_Sn_O ? H6)
808                                                   |do 2 rewrite > div_times;reflexivity]]
809                                             |reflexivity]
810                                          |reflexivity]
811                                       |apply lt_O_fact
812                                       |cut (pi_p x (λy:nat.true) (λi:nat.a-a*i/n) = (exp a x)/(exp n x)*(n!/(n-x)!))
813                                          [rewrite > Hcut3;rewrite > times_n_SO;
814                                           rewrite > sym_times;apply divides_times
815                                             [apply divides_SO_n;
816                                             |apply divides_times_to_divides_div;
817                                                [apply lt_O_fact
818                                                |apply bc2;apply le_S_S_to_le;assumption]]
819                                          |cut (pi_p x (\lambda y.true) (\lambda i. a - a*i/n) =
820                                               pi_p x (\lambda y.true) (\lambda i. a*(n-i)/n))
821                                             [rewrite > Hcut3;
822                                              rewrite < (divides_pi_p_to_eq ? ? (\lambda i.(a*(n-i))) (\lambda i.n))
823                                                [rewrite > (times_pi_p ? ? (\lambda i.a) (\lambda i.(n-i)));
824                                                 rewrite > divides_times_to_eq;
825                                                   [apply eq_f2
826                                                      [apply eq_f2;rewrite < eq_exp_pi_p;reflexivity
827                                                      |rewrite < Hcut;rewrite > H3;
828                                                       rewrite < sym_times in ⊢ (? ? ? (? (? % ?) ?));
829                                                       rewrite > (S_pred ((n-x)!));
830                                                         [rewrite > assoc_times;
831                                                          rewrite > div_times;reflexivity
832                                                         |apply lt_O_fact]]
833                                                   |unfold lt;cut (1 = pi_p x (\lambda y.true) (\lambda y.1))
834                                                      [rewrite > Hcut4;apply le_pi_p;intros;assumption
835                                                      |elim x
836                                                         [simplify;reflexivity
837                                                         |rewrite > true_to_pi_p_Sn;
838                                                            [rewrite < H4;reflexivity
839                                                            |reflexivity]]]
840                                                   |elim x
841                                                      [simplify;apply divides_SO_n
842                                                      |rewrite > true_to_pi_p_Sn
843                                                         [rewrite > true_to_pi_p_Sn
844                                                            [apply divides_times;assumption
845                                                            |reflexivity]
846                                                         |reflexivity]]]
847                                                |intros;split
848                                                   [assumption
849                                                   |rewrite > times_n_SO;apply divides_times
850                                                      [assumption
851                                                      |apply divides_SO_n]]]
852                                             |apply eq_pi_p;intros;
853                                                [reflexivity
854                                                |elim H1;rewrite > H5;rewrite > (S_pred n);
855                                                   [rewrite > assoc_times;
856                                                    rewrite > assoc_times;
857                                                    rewrite > div_times;
858                                                    rewrite > div_times;
859                                                    rewrite > distr_times_minus;
860                                                    rewrite > sym_times;
861                                                    reflexivity
862                                                   |assumption]]]]]
863                                    |intros;split
864                                       [assumption
865                                       |rewrite > sym_times;rewrite > times_n_SO;
866                                        apply divides_times
867                                          [assumption
868                                          |apply divides_SO_n]]]
869                                 |rewrite < eq_exp_pi_p;reflexivity]
870                              |apply lt_O_exp;assumption
871                              |apply lt_O_fact]
872                           |apply lt_O_fact
873                           |apply lt_O_exp;assumption]
874                        |apply lt_O_exp;assumption
875                        |rewrite > (times_pi_p ? ? (\lambda x.(n-x)) (\lambda x.a));
876                         rewrite > divides_times_to_eq
877                           [rewrite > times_n_SO;rewrite > sym_times;apply divides_times
878                              [apply divides_SO_n
879                              |elim x
880                                 [simplify;apply divides_SO_n
881                                 |change in \vdash (? % ?) with (n*(exp n n2));
882                                  rewrite > true_to_pi_p_Sn
883                                    [apply divides_times;assumption
884                                    |reflexivity]]]
885                           |apply lt_O_fact
886                           |apply (witness ? ? n1);symmetry;assumption]]
887                     |rewrite > divides_times_to_eq;
888                        [apply eq_f2
889                           [reflexivity
890                           |elim x
891                              [simplify;reflexivity
892                              |change in \vdash (? ? % ?) with (a*(exp a n2));
893                               rewrite > true_to_pi_p_Sn
894                                 [apply eq_f2
895                                    [reflexivity
896                                    |assumption]
897                                 |reflexivity]]]
898                        |apply lt_O_fact
899                        |apply (witness ? ? n1);symmetry;assumption]]
900                  |apply lt_O_fact
901                  |apply lt_O_fact]
902               |apply (inj_times_r (pred ((n-x)!)));
903                rewrite < (S_pred ((n-x)!))
904                  [rewrite < assoc_times;rewrite < sym_times in \vdash (? ? (? % ?) ?);
905                   rewrite < H3;generalize in match H2; elim x
906                     [rewrite < minus_n_O;simplify;rewrite < times_n_SO;reflexivity
907                     |rewrite < fact_minus in H4;
908                        [rewrite > true_to_pi_p_Sn
909                           [rewrite < assoc_times;rewrite > sym_times in \vdash (? ? ? (? % ?));
910                            apply H4;apply lt_to_le;assumption
911                           |reflexivity]
912                        |apply le_S_S_to_le;assumption]]
913                  |apply lt_O_fact]]
914            |apply le_S_S_to_le;assumption]
915         |apply le_n
916         |apply le_S_S_to_le;assumption]]]
917 qed.
918
919 lemma divides_sigma_p_to_eq : \forall k,p,f,b.O < b \to 
920  (\forall x.p x = true \to b \divides f x) \to
921  (sigma_p k p f)/b = sigma_p k p (\lambda x. (f x)/b).
922 intros;cut (\forall k1.b \divides sigma_p k1 p f)
923   [|intro;elim k1
924      [simplify;apply (witness ? ? O);rewrite < times_n_O;reflexivity
925      |apply (bool_elim ? (p n));intro
926         [rewrite > true_to_sigma_p_Sn;
927            [elim (H1 n);
928               [elim H2;rewrite > H4;rewrite > H5;rewrite < distr_times_plus;
929                rewrite > times_n_SO in \vdash (? % ?);apply divides_times
930                  [apply divides_n_n
931                  |apply divides_SO_n]
932               |assumption]
933            |assumption]
934         |rewrite > false_to_sigma_p_Sn;assumption]]]
935 elim k
936   [cases H;simplify;reflexivity
937   |apply (bool_elim ? (p n));intro
938      [rewrite > true_to_sigma_p_Sn
939         [rewrite > true_to_sigma_p_Sn
940            [elim (H1 n);
941               [elim (Hcut n);rewrite > H4;rewrite > H5;rewrite < distr_times_plus;
942                rewrite < H2;rewrite > H5;cases H;do 3 rewrite > div_times;
943                reflexivity
944               |assumption]
945            |assumption]
946         |assumption]
947      |do 2 try rewrite > false_to_sigma_p_Sn;assumption]]
948 qed.
949
950 lemma neper_sigma_p3 : \forall a,n.O < a \to O < n \to n \divides a \to (exp (S n) n)/(exp n n) =
951 sigma_p (S n) (\lambda x.true) 
952 (\lambda k.(exp a (n-k))*(pi_p k (\lambda y.true) (\lambda i.a - (a*i/n)))/k!)/(exp a n).
953 intros;transitivity ((exp a n)*(exp (S n) n)/(exp n n)/(exp a n))
954   [rewrite > eq_div_div_div_times
955      [rewrite < sym_times; rewrite < lt_to_lt_to_eq_div_div_times_times;
956         [reflexivity
957         |apply lt_O_exp;assumption
958         |apply lt_O_exp;assumption]
959      |apply lt_O_exp;assumption
960      |apply lt_O_exp;assumption]
961   |apply eq_f2;
962      [rewrite > times_exp;rewrite > neper_sigma_p1
963         [transitivity (sigma_p (S n) (λx:nat.true) (λk:nat.bc n k*(a)\sup(n)*(exp n (n-k))/(exp n n)))
964            [elim H2;rewrite > H3;rewrite < times_exp;rewrite > sym_times in ⊢ (? ? (? (? ? ? (λ_:?.? ? %)) ?) ?);
965             rewrite > sym_times in ⊢ (? ? ? (? ? ? (λ_:?.? (? (? ? %) ?) ?)));
966             transitivity (sigma_p (S n) (λx:nat.true)
967 (λk:nat.(exp n n)*(bc n k*(n)\sup(n-k)*(n1)\sup(n)))/exp n n)
968               [apply eq_f2
969                  [apply eq_sigma_p;intros;
970                     [reflexivity
971                     |rewrite < assoc_times;rewrite > sym_times;reflexivity]
972                  |reflexivity]
973               |rewrite < (distributive_times_plus_sigma_p ? ? ? (\lambda k.bc n k*(exp n (n-k))*(exp n1 n)));
974                transitivity (sigma_p (S n) (λx:nat.true)
975                 (λk:nat.bc n k*(n1)\sup(n)*(n)\sup(n-k)))
976                  [rewrite > (S_pred (exp n n))
977                     [rewrite > div_times;apply eq_sigma_p;intros
978                        [reflexivity
979                        |rewrite > sym_times;rewrite > sym_times in ⊢ (? ? ? (? % ?));
980                         rewrite > assoc_times in \vdash (? ? ? %);reflexivity]
981                     |apply lt_O_exp;assumption]
982                  |apply eq_sigma_p;intros
983                     [reflexivity
984                     |rewrite < assoc_times;rewrite > assoc_times in \vdash (? ? ? %);
985                      rewrite > sym_times in \vdash (? ? ? (? (? ? %) ?));
986                      rewrite < assoc_times;rewrite > sym_times in \vdash (? ? ? %);
987                      rewrite > (S_pred (exp n n))
988                        [rewrite > div_times;reflexivity
989                        |apply lt_O_exp;assumption]]]]
990            |rewrite > neper_sigma_p2;
991               [reflexivity
992               |assumption
993               |assumption]]
994         |assumption]
995      |reflexivity]]
996 qed.
997
998 theorem neper_monotonic : \forall n. O < n \to
999 (exp (S n) n)/(exp n n) \leq (exp (S (S n)) (S n))/(exp (S n) (S n)).
1000 intros;rewrite > (neper_sigma_p3 (n*S n) n)
1001   [rewrite > (neper_sigma_p3 (n*S n) (S n))
1002      [change in ⊢ (? ? (? ? %)) with ((n * S n)*(exp (n * S n) n));
1003       rewrite < eq_div_div_div_times
1004         [apply monotonic_div;
1005            [apply lt_O_exp;rewrite > (times_n_O O);apply lt_times
1006               [assumption
1007               |apply lt_O_S]
1008            |apply le_times_to_le_div
1009               [rewrite > (times_n_O O);apply lt_times
1010                  [assumption
1011                  |apply lt_O_S]
1012               |rewrite > distributive_times_plus_sigma_p;
1013                apply (trans_le ? (sigma_p (S n) (λx:nat.true)
1014                  (λk:nat.((n*S n))\sup(S n-k)*pi_p k (λy:nat.true) (λi:nat.n*S n-n*S n*i/S n)/k!)))
1015                  [apply le_sigma_p;intros;rewrite > sym_times in ⊢ (? (? ? %) ?);
1016                   rewrite > sym_times in \vdash (? ? (? % ?));
1017                   rewrite > divides_times_to_eq in \vdash (? ? %)
1018                     [rewrite > divides_times_to_eq in \vdash (? % ?)
1019                        [rewrite > sym_times in \vdash (? (? ? %) ?);
1020                         rewrite < assoc_times;
1021                         rewrite > sym_times in \vdash (? ? %);
1022                         rewrite > minus_Sn_m;
1023                           [apply le_times_r;apply monotonic_div
1024                              [apply lt_O_fact
1025                              |apply le_pi_p;intros;apply monotonic_le_minus_r;
1026                               rewrite > assoc_times in \vdash (? % ?);
1027                               rewrite > sym_times in \vdash (? % ?);
1028                               rewrite > assoc_times in \vdash (? % ?);
1029                               rewrite > div_times;
1030                               rewrite > (S_pred n) in \vdash (? ? %);
1031                                 [rewrite > assoc_times;rewrite > div_times;
1032                                  rewrite < S_pred
1033                                    [rewrite > sym_times;apply le_times_l;apply le_S;apply le_n
1034                                    |assumption]
1035                                 |assumption]]
1036                           |apply le_S_S_to_le;assumption]
1037                        |apply lt_O_fact
1038                        |cut (pi_p i (λy:nat.true) (λi:nat.n*S n-n*S n*i/n) = 
1039                              pi_p i (\lambda y.true) (\lambda i.S n) *
1040                              pi_p i (\lambda y.true) (\lambda i.(n-i)))
1041                           [rewrite > Hcut;rewrite > times_n_SO;
1042                            rewrite > sym_times;apply divides_times
1043                              [apply divides_SO_n
1044                              |elim (bc2 n i);
1045                                 [apply (witness ? ? n1);
1046                                  cut (pi_p i (\lambda y.true) (\lambda i.n-i) = (n!/(n-i)!))
1047                                    [rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?);
1048                                     rewrite > (S_pred ((n-i)!))
1049                                       [rewrite > assoc_times;rewrite > div_times;
1050                                        reflexivity
1051                                       |apply lt_O_fact]
1052                                    |generalize in match H1;elim i
1053                                       [rewrite < minus_n_O;rewrite > div_n_n;
1054                                          [reflexivity
1055                                          |apply lt_O_fact]
1056                                       |rewrite > true_to_pi_p_Sn
1057                                          [rewrite > H4
1058                                             [rewrite > sym_times;rewrite < divides_times_to_eq
1059                                                [rewrite < fact_minus
1060                                                   [rewrite > sym_times in ⊢ (? ? (? ? %) ?);
1061                                                    rewrite < lt_to_lt_to_eq_div_div_times_times;
1062                                                      [reflexivity
1063                                                      |apply lt_to_lt_O_minus;apply le_S_S_to_le;
1064                                                       assumption
1065                                                      |apply lt_O_fact;]
1066                                                   |apply le_S_S_to_le;assumption]
1067                                                |apply lt_O_fact
1068                                                |apply divides_fact_fact;
1069                                                 apply le_plus_to_minus;
1070                                                 rewrite > plus_n_O in \vdash (? % ?);
1071                                                 apply le_plus_r;apply le_O_n]
1072                                             |apply lt_to_le;assumption]
1073                                          |reflexivity]]]
1074                                 |apply le_S_S_to_le;assumption]]
1075                           |rewrite < times_pi_p;apply eq_pi_p;intros;
1076                              [reflexivity
1077                              |rewrite > distr_times_minus;rewrite > assoc_times;
1078                               rewrite > (S_pred n) in \vdash (? ? (? ? (? (? % ?) %)) ?)
1079                                 [rewrite > div_times;rewrite > sym_times;reflexivity
1080                                 |assumption]]]]
1081                     |apply lt_O_fact
1082                     |cut (pi_p i (λy:nat.true) (λi:nat.n*S n-n*S n*i/S n) = 
1083                              pi_p i (\lambda y.true) (\lambda i.n) *
1084                              pi_p i (\lambda y.true) (\lambda i.(S n-i)))
1085                           [rewrite > Hcut;rewrite > times_n_SO;rewrite > sym_times;
1086                            apply divides_times
1087                              [apply divides_SO_n
1088                              |elim (bc2 (S n) i);
1089                                 [apply (witness ? ? n1);
1090                                  cut (pi_p i (\lambda y.true) (\lambda i.S n-i) = ((S n)!/(S n-i)!))
1091                                    [rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?);
1092                                     rewrite > (S_pred ((S n-i)!))
1093                                       [rewrite > assoc_times;rewrite > div_times;
1094                                        reflexivity
1095                                       |apply lt_O_fact]
1096                                    |generalize in match H1;elim i
1097                                       [rewrite < minus_n_O;rewrite > div_n_n;
1098                                          [reflexivity
1099                                          |apply lt_O_fact]
1100                                       |rewrite > true_to_pi_p_Sn
1101                                          [rewrite > H4
1102                                             [rewrite > sym_times;rewrite < divides_times_to_eq
1103                                                [rewrite < fact_minus
1104                                                   [rewrite > sym_times in ⊢ (? ? (? ? %) ?);
1105                                                    rewrite < lt_to_lt_to_eq_div_div_times_times;
1106                                                      [reflexivity
1107                                                      |apply lt_to_lt_O_minus;apply lt_to_le;
1108                                                       assumption
1109                                                      |apply lt_O_fact]
1110                                                   |apply lt_to_le;assumption]
1111                                                |apply lt_O_fact
1112                                                |apply divides_fact_fact;
1113                                                 apply le_plus_to_minus;
1114                                                 rewrite > plus_n_O in \vdash (? % ?);
1115                                                 apply le_plus_r;apply le_O_n]
1116                                             |apply lt_to_le;assumption]
1117                                          |reflexivity]]]
1118                                 |apply lt_to_le;assumption]]
1119                           |rewrite < times_pi_p;apply eq_pi_p;intros;
1120                              [reflexivity
1121                              |rewrite > distr_times_minus;rewrite > sym_times in \vdash (? ? (? ? (? (? % ?) ?)) ?);
1122                               rewrite > assoc_times;rewrite > div_times;reflexivity]]]
1123                     |rewrite > true_to_sigma_p_Sn in \vdash (? ? %)
1124                        [rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
1125                         apply le_plus_r;apply le_O_n
1126                        |reflexivity]]]]
1127            |rewrite > (times_n_O O);apply lt_times
1128               [assumption
1129               |apply lt_O_S]
1130            |apply lt_O_exp;rewrite > (times_n_O O);apply lt_times
1131               [assumption
1132               |apply lt_O_S]]
1133         |rewrite > (times_n_O O);apply lt_times
1134            [assumption
1135            |apply lt_O_S]
1136         |apply lt_O_S
1137         |apply (witness ? ? n);apply sym_times]
1138      |rewrite > (times_n_O O);apply lt_times
1139         [assumption
1140         |apply lt_O_S]
1141      |assumption
1142      |apply (witness ? ? (S n));reflexivity]
1143 qed.
1144
1145 theorem le_SSO_neper : \forall n.O < n \to (2 \leq (exp (S n) n)/(exp n n)).
1146 intros;elim H
1147   [simplify;apply le_n
1148   |apply (trans_le ? ? ? H2);apply neper_monotonic;assumption]
1149 qed.
1150
1151 theorem le_SSO_exp_neper : \forall n.O < n \to 2*(exp n n) \leq exp (S n) n.
1152 intros;apply (trans_le ? ((exp (S n) n)/(exp n n)*(exp n n)))
1153   [apply le_times_l;apply le_SSO_neper;assumption
1154   |rewrite > sym_times;apply (trans_le ? ? ? (le_times_div_div_times ? ? ? ?))
1155      [apply lt_O_exp;assumption
1156      |cases (lt_O_exp ? n H);rewrite > div_times;apply le_n]]
1157 qed.
1158                                        
1159 (* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to
1160 divides n m \to
1161 log p (exp n m) - log p (exp a m) \le
1162 sigma_p (S n) (\lambda i.leb (S a) i) (\lambda i.S((m/i)*S(log p (S(S(S O)))))).
1163 intros.
1164 elim n
1165   [rewrite > false_to_sigma_p_Sn.
1166    simplify.
1167    apply (lt_O_n_elim ? H).intro.
1168    simplify.apply le_O_n
1169   |apply (bool_elim ? (leb a n1));intro
1170     [rewrite > true_to_sigma_p_Sn
1171       [apply (trans_le ? (S (m/S n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(m))-log p ((a)\sup(m)))))
1172         [rewrite > sym_plus. 
1173          rewrite > plus_minus
1174           [apply le_plus_to_minus_r.
1175            rewrite < plus_minus_m_m
1176             [rewrite > sym_plus.
1177              apply le_log_exp_Sn_log_exp_n.
1178
1179
1180 * a generalization 
1181 theorem le_exp_sigma_p_exp_m: \forall m,n. (exp (S m) n) \le
1182 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
1183 intros.
1184 rewrite > exp_S_sigma_p.
1185 apply le_sigma_p.
1186 intros.unfold bc.
1187 apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
1188   [rewrite > sym_times.
1189    apply le_times_r.
1190    rewrite > sym_times.
1191    rewrite < eq_div_div_div_times
1192     [apply monotonic_div
1193       [apply lt_O_fact
1194       |apply le_times_to_le_div2
1195         [apply lt_O_fact
1196         |apply le_fact_exp.
1197          apply le_S_S_to_le.
1198          assumption
1199         ]
1200       ]
1201     |apply lt_O_fact
1202     |apply lt_O_fact
1203     ]
1204   |apply le_times_div_div_times.
1205    apply lt_O_fact
1206   ]
1207 qed.
1208
1209 theorem lt_exp_sigma_p_exp_m: \forall m,n. S O < n \to
1210 (exp (S m) n) <
1211 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
1212 intros.
1213 rewrite > exp_S_sigma_p.
1214 apply lt_sigma_p
1215   [intros.unfold bc.
1216    apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
1217     [rewrite > sym_times.
1218      apply le_times_r.
1219      rewrite > sym_times.
1220      rewrite < eq_div_div_div_times
1221       [apply monotonic_div
1222         [apply lt_O_fact
1223         |apply le_times_to_le_div2
1224           [apply lt_O_fact
1225           |apply le_fact_exp.
1226            apply le_S_S_to_le.
1227            assumption
1228           ]
1229         ]
1230       |apply lt_O_fact
1231       |apply lt_O_fact
1232       ]
1233     |apply le_times_div_div_times.
1234      apply lt_O_fact
1235     ]
1236   |apply (ex_intro ? ? n).
1237    split
1238     [split
1239       [apply le_n
1240       |reflexivity
1241       ]
1242     |rewrite < minus_n_n.
1243      rewrite > bc_n_n.
1244      simplify.unfold lt.
1245      apply le_times_to_le_div
1246       [apply lt_O_fact
1247       |rewrite > sym_times.
1248        rewrite < plus_n_O.
1249        apply le_fact_exp1.
1250        assumption
1251       ]
1252     ]
1253   ]
1254 qed.
1255    
1256 theorem lt_SO_to_lt_exp_Sn_n_SSSO_bof: \forall m,n. S O < n \to 
1257 (exp (S m) n) < (S(S(S O)))*(exp m n).
1258 intros.  
1259 apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!))))
1260   [apply lt_exp_sigma_p_exp_m.assumption
1261   |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
1262     [apply le_sigma_p.intros.
1263      apply le_times_to_le_div
1264       [apply lt_O_exp.
1265        apply lt_O_S
1266       |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
1267         [apply le_times_div_div_times.
1268          apply lt_O_fact
1269         |apply le_times_to_le_div2
1270           [apply lt_O_fact
1271           |rewrite < sym_times.
1272            apply le_times_r.
1273            apply le_exp_SSO_fact
1274           ]
1275         ]
1276       ]
1277     |rewrite > eq_sigma_p_pred
1278       [rewrite > div_SO.
1279        rewrite > sym_plus.
1280        change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
1281        apply le_plus_r.
1282        apply (trans_le ? (((S(S O))*(exp n n)*(exp (S(S O)) n) - (S(S O))*(exp n n))/(exp (S(S O)) n)))
1283         [apply sigma_p_div_exp
1284         |apply le_times_to_le_div2
1285           [apply lt_O_exp.
1286            apply lt_O_S.
1287           |apply le_minus_m
1288           ]
1289         ]
1290       |reflexivity
1291       ]
1292     ]
1293   ]
1294 qed.     
1295 *)