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 set "baseuri" "cic:/matita/nat/neper".
  16
  17 include "nat/iteration2.ma".
  18 include "nat/div_and_mod_diseq.ma".
  19 include "nat/binomial.ma".
  20 include "nat/log.ma".
  21 include "nat/chebyshev.ma".
  22
  23 theorem sigma_p_div_exp: \forall n,m.
  24 sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le
  25 ((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
  26 intros.
  27 elim n
  28   [apply le_O_n.
  29   |rewrite > true_to_sigma_p_Sn
  30     [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)))
  31       [apply le_plus_r.assumption
  32       |rewrite > assoc_times in ⊢ (? ? (? (? % ?) ?)).
  33        rewrite < distr_times_minus.
  34        change in ⊢ (? ? (? ? %)) with ((S(S O))*(exp (S(S O)) n1)).
  35        rewrite > sym_times in ⊢ (? ? (? % ?)).
  36        rewrite > sym_times in ⊢ (? ? (? ? %)).
  37        rewrite < lt_to_lt_to_eq_div_div_times_times
  38         [apply (trans_le ? ((m+((S(S O))*m*((S(S O)))\sup(n1)-(S(S O))*m))/((S(S O)))\sup(n1)))
  39           [apply le_plus_div.
  40            apply lt_O_exp.
  41            apply lt_O_S
  42           |change in ⊢ (? (? (? ? (? ? %)) ?) ?) with (m + (m +O)).
  43            rewrite < plus_n_O.
  44            rewrite < eq_minus_minus_minus_plus.
  45            rewrite > sym_plus.
  46            rewrite > sym_times in ⊢ (? (? (? (? (? (? % ?) ?) ?) ?) ?) ?).
  47            rewrite > assoc_times.
  48            rewrite < plus_minus_m_m
  49             [apply le_n
  50             |apply le_plus_to_minus_r.
  51              rewrite > plus_n_O in ⊢ (? (? ? %) ?).
  52              change in ⊢ (? % ?) with ((S(S O))*m).
  53              rewrite > sym_times.
  54              apply le_times_r.
  55              rewrite > times_n_SO in ⊢ (? % ?).
  56              apply le_times_r.
  57              apply lt_O_exp.
  58              apply lt_O_S
  59             ]
  60           ]
  61         |apply lt_O_S
  62         |apply lt_O_exp.
  63          apply lt_O_S
  64         ]
  65       ]
  66     |reflexivity
  67     ]
  68   ]
  69 qed.
  70
  71 theorem le_fact_exp: \forall i,m. i \le m \to m!≤ m \sup i*(m-i)!.
  72 intro.elim i
  73   [rewrite < minus_n_O.
  74    simplify.rewrite < plus_n_O.
  75    apply le_n
  76   |simplify.
  77    apply (trans_le ? ((m)\sup(n)*(m-n)!))
  78     [apply H.
  79      apply lt_to_le.assumption
  80     |rewrite > sym_times in ⊢ (? ? (? % ?)).
  81      rewrite > assoc_times.
  82      apply le_times_r.
  83      generalize in match H1.
  84      cases m;intro
  85       [apply False_ind.
  86        apply (lt_to_not_le ? ? H2).
  87        apply le_O_n
  88       |rewrite > minus_Sn_m.
  89        simplify.
  90        apply le_plus_r.
  91        apply le_times_l.
  92        apply le_minus_m.
  93        apply le_S_S_to_le.
  94        assumption
  95       ]
  96     ]
  97   ]
  98 qed.
  99
 100 theorem le_fact_exp1: \forall n. S O < n \to (S(S O))*n!≤ n \sup n.
 101 intros.elim H
 102   [apply le_n
 103   |change with ((S(S O))*((S n1)*(fact n1)) \le (S n1)*(exp (S n1) n1)).
 104    rewrite < assoc_times.
 105    rewrite < sym_times in ⊢ (? (? % ?) ?).
 106    rewrite > assoc_times.
 107    apply le_times_r.
 108    apply (trans_le ? (exp n1 n1))
 109     [assumption
 110     |apply monotonic_exp1.
 111      apply le_n_Sn
 112     ]
 113   ]
 114 qed.
 115
 116 theorem le_exp_sigma_p_exp: \forall n. (exp (S n) n) \le
 117 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
 118 intro.
 119 rewrite > exp_S_sigma_p.
 120 apply le_sigma_p.
 121 intros.unfold bc.
 122 apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
 123   [rewrite > sym_times.
 124    apply le_times_r.
 125    rewrite > sym_times.
 126    rewrite < eq_div_div_div_times
 127     [apply monotonic_div
 128       [apply lt_O_fact
 129       |apply le_times_to_le_div2
 130         [apply lt_O_fact
 131         |apply le_fact_exp.
 132          apply le_S_S_to_le.
 133          assumption
 134         ]
 135       ]
 136     |apply lt_O_fact
 137     |apply lt_O_fact
 138     ]
 139   |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
 140     [rewrite > exp_plus_times.
 141      apply le_times_div_div_times.
 142      apply lt_O_fact
 143     |apply le_S_S_to_le.
 144      assumption
 145     ]
 146   ]
 147 qed.
 148
 149 theorem lt_exp_sigma_p_exp: \forall n. S O < n \to
 150 (exp (S n) n) <
 151 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
 152 intros.
 153 rewrite > exp_S_sigma_p.
 154 apply lt_sigma_p
 155   [intros.unfold bc.
 156    apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
 157     [rewrite > sym_times.
 158      apply le_times_r.
 159      rewrite > sym_times.
 160      rewrite < eq_div_div_div_times
 161       [apply monotonic_div
 162         [apply lt_O_fact
 163         |apply le_times_to_le_div2
 164           [apply lt_O_fact
 165           |apply le_fact_exp.
 166            apply le_S_S_to_le.
 167            assumption
 168           ]
 169         ]
 170       |apply lt_O_fact
 171       |apply lt_O_fact
 172       ]
 173     |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
 174       [rewrite > exp_plus_times.
 175        apply le_times_div_div_times.
 176        apply lt_O_fact
 177       |apply le_S_S_to_le.
 178        assumption
 179       ]
 180     ]
 181   |apply (ex_intro ? ? n).
 182    split
 183     [split
 184       [apply le_n
 185       |reflexivity
 186       ]
 187     |rewrite < minus_n_n.
 188      rewrite > bc_n_n.
 189      simplify.unfold lt.
 190      apply le_times_to_le_div
 191       [apply lt_O_fact
 192       |rewrite > sym_times.
 193        apply le_fact_exp1.
 194        assumption
 195       ]
 196     ]
 197   ]
 198 qed.
 199
 200 theorem le_exp_SSO_fact:\forall n.
 201 exp (S(S O)) (pred n) \le n!.
 202 intro.elim n
 203   [apply le_n
 204   |change with ((S(S O))\sup n1 ≤(S n1)*n1!).
 205    apply (nat_case1 n1);intros
 206     [apply le_n
 207     |change in ⊢ (? % ?) with ((S(S O))*exp (S(S O)) (pred (S m))).
 208      apply le_times
 209       [apply le_S_S.apply le_S_S.apply le_O_n
 210       |rewrite < H1.assumption
 211       ]
 212     ]
 213   ]
 214 qed.
 215
 216 theorem lt_SO_to_lt_exp_Sn_n_SSSO: \forall n. S O < n \to
 217 (exp (S n) n) < (S(S(S O)))*(exp n n).
 218 intros.
 219 apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
 220   [apply lt_exp_sigma_p_exp.assumption
 221   |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
 222     [apply le_sigma_p.intros.
 223      apply le_times_to_le_div
 224       [apply lt_O_exp.
 225        apply lt_O_S
 226       |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
 227         [apply le_times_div_div_times.
 228          apply lt_O_fact
 229         |apply le_times_to_le_div2
 230           [apply lt_O_fact
 231           |rewrite < sym_times.
 232            apply le_times_r.
 233            apply le_exp_SSO_fact
 234           ]
 235         ]
 236       ]
 237     |rewrite > eq_sigma_p_pred
 238       [rewrite > div_SO.
 239        rewrite > sym_plus.
 240        change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
 241        apply le_plus_r.
 242        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)))
 243         [apply sigma_p_div_exp
 244         |apply le_times_to_le_div2
 245           [apply lt_O_exp.
 246            apply lt_O_S.
 247           |apply le_minus_m
 248           ]
 249         ]
 250       |reflexivity
 251       ]
 252     ]
 253   ]
 254 qed.
 255
 256 theorem lt_exp_Sn_n_SSSO: \forall n.
 257 (exp (S n) n) < (S(S(S O)))*(exp n n).
 258 intro.cases n;intros
 259   [simplify.apply le_S.apply le_n
 260   |cases n1;intros
 261     [simplify.apply le_n
 262     |apply lt_SO_to_lt_exp_Sn_n_SSSO.
 263      apply le_S_S.apply le_S_S.apply le_O_n
 264     ]
 265   ]
 266 qed.
 267
 268 theorem lt_exp_Sn_m_SSSO: \forall n,m. O < m \to
 269 divides n m \to
 270 (exp (S n) m) < (exp (S(S(S O))) (m/n)) *(exp n m).
 271 intros.
 272 elim H1.rewrite > H2.
 273 rewrite < exp_exp_times.
 274 rewrite < exp_exp_times.
 275 rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?)).
 276 rewrite > lt_O_to_div_times
 277   [rewrite > times_exp.
 278    apply lt_exp1
 279     [apply (O_lt_times_to_O_lt ? n).
 280      rewrite > sym_times.
 281      rewrite < H2.
 282      assumption
 283     |apply lt_exp_Sn_n_SSSO
 284     ]
 285   |apply (O_lt_times_to_O_lt ? n2).
 286    rewrite < H2.
 287    assumption
 288   ]
 289 qed.
 290
 291 theorem le_log_exp_Sn_log_exp_n: \forall n,m,p. O < m \to S O < p \to
 292 divides n m \to
 293 log p (exp (S n) m) \le S((m/n)*S(log p (S(S(S O))))) + log p (exp n m).
 294 intros.
 295 apply (trans_le ? (log p (((S(S(S O))))\sup(m/n)*((n)\sup(m)))))
 296   [apply le_log
 297     [assumption
 298     |apply lt_to_le.
 299      apply lt_exp_Sn_m_SSSO;assumption
 300     ]
 301   |apply (trans_le ? (S(log p (exp (S(S(S O))) (m/n)) + log p (exp n m))))
 302     [apply log_times.
 303      assumption
 304     |change in ⊢ (? ? %) with (S (m/n*S (log p (S(S(S O))))+log p ((n)\sup(m)))).
 305      apply le_S_S.
 306      apply le_plus_l.
 307      apply log_exp1.
 308      assumption
 309     ]
 310   ]
 311 qed.
 312
 313 theorem le_log_exp_fact_sigma_p: \forall a,b,n,p. S O < p \to
 314 O < a \to a \le b \to b \le n \to
 315 log p (exp b n!) - log p (exp a n!) \le
 316 sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))).
 317 intros 7.
 318 elim b
 319   [simplify.
 320    apply (lt_O_n_elim ? (lt_O_fact n)).intro.
 321    apply le_n.
 322   |apply (bool_elim ? (leb a n1));intro
 323     [rewrite > true_to_sigma_p_Sn
 324       [apply (trans_le ? (S (n!/n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(n!))-log p ((a)\sup(n!)))))
 325         [rewrite > sym_plus.
 326          rewrite > plus_minus
 327           [apply le_plus_to_minus_r.
 328            rewrite < plus_minus_m_m
 329             [rewrite > sym_plus.
 330              apply le_log_exp_Sn_log_exp_n
 331               [apply lt_O_fact
 332               |assumption
 333               |apply divides_fact;
 334                  [apply (trans_le ? ? ? H1);apply leb_true_to_le;assumption
 335                  |apply lt_to_le;assumption]]
 336             |apply le_log
 337               [assumption
 338               |cut (O = exp O n!)
 339                  [rewrite > Hcut;apply monotonic_exp1;constructor 2;
 340                   apply leb_true_to_le;assumption
 341                  |elim n
 342                     [reflexivity
 343                     |simplify;rewrite > exp_plus_times;rewrite < H6;
 344                      rewrite > sym_times;rewrite < times_n_O;reflexivity]]]]
 345         |apply le_log
 346           [assumption
 347           |apply monotonic_exp1;apply leb_true_to_le;assumption]]
 348       |rewrite > sym_plus;rewrite > sym_plus in \vdash (? ? %);apply le_minus_to_plus;
 349        rewrite < minus_plus_m_m;apply H3;apply lt_to_le;assumption]
 350     |assumption]
 351   |lapply (not_le_to_lt ? ? (leb_false_to_not_le ? ? H5));
 352    rewrite > eq_minus_n_m_O
 353     [apply le_O_n
 354     |apply le_log
 355        [assumption
 356        |apply monotonic_exp1;assumption]]]]
 357 qed.
 358
 359 theorem le_exp_div:\forall n,m,q. O < m \to
 360 exp (n/m) q \le (exp n q)/(exp m q).
 361 intros.
 362 apply le_times_to_le_div
 363   [apply lt_O_exp.
 364    assumption
 365   |rewrite > times_exp.
 366    rewrite < sym_times.
 367    apply monotonic_exp1.
 368    rewrite > (div_mod n m) in ⊢ (? ? %)
 369     [apply le_plus_n_r
 370     |assumption
 371     ]
 372   ]
 373 qed.
 374
 375 theorem le_log_div_sigma_p: \forall a,b,n,p. S O < p \to
 376 O < a \to a \le b \to b \le n \to
 377 log p (b/a) \le
 378 (sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))))/n!.
 379 intros.
 380 apply le_times_to_le_div
 381   [apply lt_O_fact
 382   |apply (trans_le ? (log p (exp (b/a) n!)))
 383     [apply log_exp2
 384       [assumption
 385       |apply le_times_to_le_div
 386         [assumption
 387         |rewrite < times_n_SO.
 388          assumption
 389         ]
 390       ]
 391     |apply (trans_le ? (log p ((exp b n!)/(exp a n!))))
 392       [apply le_log
 393         [assumption
 394         |apply le_exp_div.assumption
 395         ]
 396       |apply (trans_le ? (log p (exp b n!) - log p (exp a n!)))
 397         [apply log_div
 398           [assumption
 399           |apply lt_O_exp.
 400            assumption
 401           |apply monotonic_exp1.
 402            assumption
 403           ]
 404         |apply le_log_exp_fact_sigma_p;assumption
 405         ]
 406       ]
 407     ]
 408   ]
 409 qed.
 410
 411 theorem sigma_p_log_div: \forall n,b. S O < b \to
 412 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
 413 \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!
 414 ).
 415 intros.
 416 apply le_sigma_p.intros.
 417 apply le_log_div_sigma_p
 418   [assumption
 419   |apply prime_to_lt_O.
 420    apply primeb_true_to_prime.
 421    apply (andb_true_true ? ? H2)
 422   |apply le_S_S_to_le.
 423    assumption
 424   |apply le_n
 425   ]
 426 qed.
 427
 428 theorem sigma_p_log_div1: \forall n,b. S O < b \to
 429 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
 430 \le
 431 (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 intros.
 433 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!
 434 )))
 435   [apply sigma_P_log_div.assumption
 436   |apply le_times_to_le_div
 437     [apply lt_O_fact
 438     |rewrite > distributive_times_plus_sigma_p.
 439      rewrite < sym_times in ⊢ (? ? %).
 440      rewrite > distributive_times_plus_sigma_p.
 441      apply le_sigma_p.intros.
 442      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!)))
 443       [apply le_times_div_div_times.
 444        apply lt_O_fact
 445       |rewrite > sym_times.
 446        rewrite > lt_O_to_div_times
 447         [rewrite > distributive_times_plus_sigma_p.
 448          apply le_sigma_p.intros.
 449          rewrite < times_n_Sm in ⊢ (? ? %).
 450          rewrite > plus_n_SO.
 451          rewrite > sym_plus.
 452          apply le_plus
 453           [apply le_S_S.apply le_O_n
 454           |rewrite < sym_times.
 455            apply le_n
 456           ]
 457         |apply lt_O_fact
 458         ]
 459       ]
 460     ]
 461   ]
 462 qed.
 463
 464 (*
 465 theorem sigma_p_log_div: \forall n,b. S O < b \to
 466 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
 467 \le (sigma_p (S n) (\lambda i.leb (S n) (i*i)) (\lambda i.(prim i)*n!/i))*S(log b (S(S(S O)))/n!
 468 ).
 469 intros.
 470 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!))
 471   [apply sigma_p_log_div1
 472   |unfold prim.
 473 *)
 474
 475
 476 (* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to
 477 divides n m \to
 478 log p (exp n m) - log p (exp a m) \le
 479 sigma_p (S n) (\lambda i.leb (S a) i) (\lambda i.S((m/i)*S(log p (S(S(S O)))))).
 480 intros.
 481 elim n
 482   [rewrite > false_to_sigma_p_Sn.
 483    simplify.
 484    apply (lt_O_n_elim ? H).intro.
 485    simplify.apply le_O_n
 486   |apply (bool_elim ? (leb a n1));intro
 487     [rewrite > true_to_sigma_p_Sn
 488       [apply (trans_le ? (S (m/S n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(m))-log p ((a)\sup(m)))))
 489         [rewrite > sym_plus.
 490          rewrite > plus_minus
 491           [apply le_plus_to_minus_r.
 492            rewrite < plus_minus_m_m
 493             [rewrite > sym_plus.
 494              apply le_log_exp_Sn_log_exp_n.
 495
 496
 497 * a generalization
 498 theorem le_exp_sigma_p_exp_m: \forall m,n. (exp (S m) n) \le
 499 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
 500 intros.
 501 rewrite > exp_S_sigma_p.
 502 apply le_sigma_p.
 503 intros.unfold bc.
 504 apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
 505   [rewrite > sym_times.
 506    apply le_times_r.
 507    rewrite > sym_times.
 508    rewrite < eq_div_div_div_times
 509     [apply monotonic_div
 510       [apply lt_O_fact
 511       |apply le_times_to_le_div2
 512         [apply lt_O_fact
 513         |apply le_fact_exp.
 514          apply le_S_S_to_le.
 515          assumption
 516         ]
 517       ]
 518     |apply lt_O_fact
 519     |apply lt_O_fact
 520     ]
 521   |apply le_times_div_div_times.
 522    apply lt_O_fact
 523   ]
 524 qed.
 525
 526 theorem lt_exp_sigma_p_exp_m: \forall m,n. S O < n \to
 527 (exp (S m) n) <
 528 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
 529 intros.
 530 rewrite > exp_S_sigma_p.
 531 apply lt_sigma_p
 532   [intros.unfold bc.
 533    apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
 534     [rewrite > sym_times.
 535      apply le_times_r.
 536      rewrite > sym_times.
 537      rewrite < eq_div_div_div_times
 538       [apply monotonic_div
 539         [apply lt_O_fact
 540         |apply le_times_to_le_div2
 541           [apply lt_O_fact
 542           |apply le_fact_exp.
 543            apply le_S_S_to_le.
 544            assumption
 545           ]
 546         ]
 547       |apply lt_O_fact
 548       |apply lt_O_fact
 549       ]
 550     |apply le_times_div_div_times.
 551      apply lt_O_fact
 552     ]
 553   |apply (ex_intro ? ? n).
 554    split
 555     [split
 556       [apply le_n
 557       |reflexivity
 558       ]
 559     |rewrite < minus_n_n.
 560      rewrite > bc_n_n.
 561      simplify.unfold lt.
 562      apply le_times_to_le_div
 563       [apply lt_O_fact
 564       |rewrite > sym_times.
 565        rewrite < plus_n_O.
 566        apply le_fact_exp1.
 567        assumption
 568       ]
 569     ]
 570   ]
 571 qed.
 572
 573 theorem lt_SO_to_lt_exp_Sn_n_SSSO_bof: \forall m,n. S O < n \to
 574 (exp (S m) n) < (S(S(S O)))*(exp m n).
 575 intros.
 576 apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!))))
 577   [apply lt_exp_sigma_p_exp_m.assumption
 578   |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
 579     [apply le_sigma_p.intros.
 580      apply le_times_to_le_div
 581       [apply lt_O_exp.
 582        apply lt_O_S
 583       |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
 584         [apply le_times_div_div_times.
 585          apply lt_O_fact
 586         |apply le_times_to_le_div2
 587           [apply lt_O_fact
 588           |rewrite < sym_times.
 589            apply le_times_r.
 590            apply le_exp_SSO_fact
 591           ]
 592         ]
 593       ]
 594     |rewrite > eq_sigma_p_pred
 595       [rewrite > div_SO.
 596        rewrite > sym_plus.
 597        change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
 598        apply le_plus_r.
 599        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)))
 600         [apply sigma_p_div_exp
 601         |apply le_times_to_le_div2
 602           [apply lt_O_exp.
 603            apply lt_O_S.
 604           |apply le_minus_m
 605           ]
 606         ]
 607       |reflexivity
 608       ]
 609     ]
 610   ]
 611 qed.
 612 *)