weblib/arithmetics/factorial.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/exp.ma".
  13
  14 let rec fact n ≝
  15   match n with
  16   [ O ⇒ \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6
  17   | S m ⇒ fact m \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m].
  18
  19 interpretation "factorial" 'fact n = (fact n).
  20
  21 theorem le_1_fact : ∀n. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
  22 #n (elim n) normalize /2/
  23 qed.
  24
  25 theorem le_2_fact : ∀n. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
  26 #n (cases n)
  27   [#abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/
  28   |#m normalize #le2 @(\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 ? \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6) //
  29   ]
  30 qed.
  31
  32 theorem le_n_fact_n: ∀n. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
  33 #n (elim n) normalize //
  34 #n #Hind @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))) // @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 //
  35 qed.
  36
  37 theorem lt_n_fact_n: ∀n. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
  38 #n (cases n)
  39   [#H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/
  40   |#m #lt2 normalize @(\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m))) //
  41    @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 // @\ 5a href="cic:/matita/arithmetics/factorial/le_2_fact.def(12)"\ 6le_2_fact\ 5/a\ 6 /2/
  42 qed.
  43
  44 (* approximations *)
  45
  46 theorem fact_to_exp1: ∀n.\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6n →
  47  (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
  48 #n #posn (cut (∀i.\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6i)))) [//] #H (elim posn) //
  49 #n #posn #Hind @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? ((\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))))
  50   [>H normalize @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 //
  51   |cut (\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))))
  52     [>\ 5a href="cic:/matita/arithmetics/nat/S_pred.def(3)"\ 6S_pred\ 5/a\ 6 // @(\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 ? \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6) //] #H1
  53    cut (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6)
  54     [>H1 >H1 //] #H2 >H2
  55    @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? ((\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))))
  56     [@\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6[@\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 //]//
  57     (* we generalize to hide the computational content *)
  58     |normalize in match ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6) generalize in match (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)
  59      #Sn generalize in match \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 #two //
  60     ]
  61   ]
  62 qed.
  63
  64 theorem fact_to_exp: ∀n.
  65  (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
  66 #n (cases n) [normalize // |#n @\ 5a href="cic:/matita/arithmetics/factorial/fact_to_exp1.def(12)"\ 6fact_to_exp1\ 5/a\ 6 //]
  67 qed.
  68
  69 theorem exp_to_fact1: ∀n.\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n →
  70   \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
  71 #n #posn (elim posn) [normalize //]
  72 #n #posn #Hind (cut (∀i.\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6i)))) [//] #H
  73 cut (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6) [>H //] #H1 >H1
  74 @(\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(5)"\ 6le_to_lt_to_lt\ 5/a\ 6 ? (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))))
  75   [normalize in match ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6) generalize in match (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) #Sn
  76    generalize in match \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 #two //
  77   |cut ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)))\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)))))
  78    [>H //] #H2 >H2 @\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"\ 6lt_to_le_to_lt_times\ 5/a\ 6
  79      [@\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"\ 6lt_to_le_to_lt_times\ 5/a\ 6 //|>H // | //]
  80   ]
  81 qed.\ 5/a\ 6
  82
  83 (* a slightly better result
  84 theorem fact3: \forall n.O < n \to
  85 (exp 2 (2*n))*(exp (fact n) 2) \le 2*n*fact (2*n).
  86 intros.
  87 elim H
  88   [simplify.apply le_n
  89   |rewrite > times_SSO.
  90    rewrite > factS.
  91    rewrite < times_exp.
  92    change in ⊢ (? (? % ?) ?) with ((S(S O))*((S(S O))*(exp (S(S O)) ((S(S O))*n1)))).
  93    rewrite > assoc_times.
  94    rewrite > assoc_times in ⊢ (? (? ? %) ?).
  95    rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
  96    rewrite < sym_times in ⊢ (? (? ? (? ? (? % ?))) ?).
  97    rewrite > assoc_times in ⊢ (? (? ? (? ? %)) ?).
  98    apply (trans_le ? (((S(S O))*((S(S O))*((S n1)\sup((S(S O)))*((S(S O))*n1*((S(S O))*n1)!))))))
  99     [apply le_times_r.
 100      apply le_times_r.
 101      apply le_times_r.
 102      assumption
 103     |rewrite > factS.
 104      rewrite > factS.
 105      rewrite < times_SSO.
 106      rewrite > assoc_times in ⊢ (? ? %).
 107      apply le_times_r.
 108      rewrite < assoc_times.
 109      change in ⊢ (? (? (? ? %) ?) ?) with ((S n1)*((S n1)*(S O))).
 110      rewrite < assoc_times in ⊢ (? (? % ?) ?).
 111      rewrite < times_n_SO.
 112      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
 113      rewrite < assoc_times in ⊢ (? ? %).
 114      rewrite < assoc_times in ⊢ (? ? (? % ?)).
 115      apply le_times_r.
 116      apply le_times_l.
 117      apply le_S.apply le_n
 118     ]
 119   ]
 120 qed.
 121
 122 theorem le_fact_10: fact (2*5) \le (exp 2 ((2*5)-2))*(fact 5)*(fact 5).
 123 simplify in \vdash (? (? %) ?).
 124 rewrite > factS in \vdash (? % ?).
 125 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash(? % ?).
 126 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
 127 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
 128 rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
 129 apply le_times_l.
 130 apply leb_true_to_le.reflexivity.
 131 qed.
 132
 133 theorem ab_times_cd: \forall a,b,c,d.(a*b)*(c*d)=(a*c)*(b*d).
 134 intros.
 135 rewrite > assoc_times.
 136 rewrite > assoc_times.
 137 apply eq_f.
 138 rewrite < assoc_times.
 139 rewrite < assoc_times.
 140 rewrite > sym_times in \vdash (? ? (? % ?) ?).
 141 reflexivity.
 142 qed.
 143
 144 (* an even better result *)
 145 theorem lt_SSSSO_to_fact: \forall n.4<n \to
 146 fact (2*n) \le (exp 2 ((2*n)-2))*(fact n)*(fact n).
 147 intros.elim H
 148   [apply le_fact_10
 149   |rewrite > times_SSO.
 150    change in \vdash (? ? (? (? (? ? %) ?) ?)) with (2*n1 - O);
 151    rewrite < minus_n_O.
 152    rewrite > factS.
 153    rewrite > factS.
 154    rewrite < assoc_times.
 155    rewrite > factS.
 156    apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
 157     [apply le_times_l.
 158      rewrite > times_SSO.
 159      apply le_times_r.
 160      apply le_n_Sn
 161     |apply (trans_le ? (2*S n1*(2*S n1)*(2\sup(2*n1-2)*n1!*n1!)))
 162       [apply le_times_r.assumption
 163       |rewrite > assoc_times.
 164        rewrite > ab_times_cd in \vdash (? (? ? %) ?).
 165        rewrite < assoc_times.
 166        apply le_times_l.
 167        rewrite < assoc_times in \vdash (? (? ? %) ?).
 168        rewrite > ab_times_cd.
 169        apply le_times_l.
 170        rewrite < exp_S.
 171        rewrite < exp_S.
 172        apply le_exp
 173         [apply lt_O_S
 174         |rewrite > eq_minus_S_pred.
 175          rewrite < S_pred
 176           [rewrite > eq_minus_S_pred.
 177            rewrite < S_pred
 178             [rewrite < minus_n_O.
 179              apply le_n
 180             |elim H1;simplify
 181               [apply lt_O_S
 182               |apply lt_O_S
 183               ]
 184             ]
 185           |elim H1;simplify
 186             [apply lt_O_S
 187             |rewrite < plus_n_Sm.
 188              rewrite < minus_n_O.
 189              apply lt_O_S
 190             ]
 191           ]
 192         ]
 193       ]
 194     ]
 195   ]
 196 qed. *)
 197
 198