commit by user utente

diff --git a/weblib/arithmetics/congruence.ma b/weblib/arithmetics/congruence.ma
index d1afc19eec57ae6674c1d5e67e06e453ef88998d..6217aa57c3d61fc73cb29b8707572bc05dd4196a 100644 (file)
--- a/weblib/arithmetics/congruence.ma
+++ b/weblib/arithmetics/congruence.ma
@@ -12,11 +12,11 @@
 include "arithmetics/primes.ma".
 
 (* successor mod n *)
-definition S_mod: nat → nat → nat ≝
-λn,m:nat. (S m) \mod n.
+definition S_mod: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 ≝
+λn,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 n.
 
-definition congruent: nat → nat → nat → Prop ≝
-λn,m,p:nat. mod n p = mod m p.
+definition congruent: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝
+λn,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 n p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 m p.
 
 interpretation "congruent" 'congruent n m p = (congruent n m p).
 
@@ -24,84 +24,84 @@ notation "hvbox(n break ≅_{p} m)"
   non associative with precedence 45
   for @{ 'congruent $n $m $p }.
   
-theorem congruent_n_n: ∀n,p:nat.n ≅_{p} n .
+theorem congruent_n_n: ∀n,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6≅\ 5/a\ 6_{p} n .
 // qed.
 
 theorem transitive_congruent: 
-  ∀p.transitive nat (λn,m.congruent n m p).
+  ∀p.\ 5a href="cic:/matita/basics/relations/transitive.def(2)"\ 6transitive\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 (λn,m.\ 5a href="cic:/matita/arithmetics/congruence/congruent.def(4)"\ 6congruent\ 5/a\ 6 n m p).
 /2/ qed.
 
-theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m.
-#n #m #ltnm @(div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
-% // @lt_mod_m_m @(ltn_to_ltO … ltnm) 
+theorem le_to_mod: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m.
+#n #m #ltnm @(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(10)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 n m \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 n (n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6m) (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 m))
+% // @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 @(\ 5a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(6)"\ 6ltn_to_ltO\ 5/a\ 6 … ltnm) 
 qed.
 
-theorem mod_mod : ∀n,p:nat. O<p → n \mod p = (n \mod p) \mod p.
-#n #p #posp >(div_mod (n \mod p) p) in ⊢ (? ? % ?) 
->(eq_div_O ? p) // @lt_mod_m_m //
+theorem mod_mod : ∀n,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 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\ 6p → n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p.
+#n #p #posp >(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p) p) in ⊢ (? ? % ?) 
+>(\ 5a href="cic:/matita/arithmetics/div_and_mod/eq_div_O.def(14)"\ 6eq_div_O\ 5/a\ 6 ? p) // @\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 //
 qed.
 
-theorem mod_times_mod : ∀n,m,p:nat. O<p → O<m → 
-  n \mod p = (n \mod (m*p)) \mod p.
+theorem mod_times_mod : ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 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\ 6p → \ 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\ 6m → 
+  n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 (m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p)) \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p.
 #n #m #p #posp #posm
-@(div_mod_spec_to_eq2 n p (n/p) (n \mod p) 
-(n/(m*p)*m + (n \mod (m*p)/p))) 
-  [@div_mod_spec_div_mod //
-  |% [@lt_mod_m_m //] >distributive_times_plus_r
-   >associative_plus <div_mod >associative_times <div_mod //
+@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(10)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 n p (n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p) (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p) 
+(n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6(m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 (m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p)\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p))) 
+  [@\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 //
+  |% [@\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 //] >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"\ 6distributive_times_plus_r\ 5/a\ 6
+   >\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/nat/associative_times.def(10)"\ 6associative_times\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 //
   ]
 qed.
 
-theorem congruent_n_mod_n : ∀n,p:nat. O < p →
- n ≅_{p} (n \mod p).
+theorem congruent_n_mod_n : ∀n,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 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 p →
+ n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6≅\ 5/a\ 6_{p} (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p).
 /2/ qed.
 
-theorem congruent_n_mod_times : ∀n,m,p:nat. O < p → O < m → 
-  n ≅_{p} (n \mod (m*p)).
+theorem congruent_n_mod_times : ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 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 p → \ 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 m → 
+  n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6≅\ 5/a\ 6_{p} (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 (m\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p)).
 /2/ qed.
 
-theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. O< p → 
-  n = r*p+m → n ≅_{p} m .
+theorem eq_times_plus_to_congruent: ∀n,m,p,r:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 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 p → 
+  n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 r\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m → n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6≅\ 5/a\ 6_{p} m .
 #n #m #p #r #posp #eqn
-@(div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
-  [@div_mod_spec_div_mod //
-  |% [@lt_mod_m_m //] >distributive_times_plus_r
-   >associative_plus <div_mod //
+@(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(10)"\ 6div_mod_spec_to_eq2\ 5/a\ 6 n p (\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 n p) (\ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 n p) (r \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 m p)) (\ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 m p))
+  [@\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_div_mod.def(13)"\ 6div_mod_spec_div_mod\ 5/a\ 6 //
+  |% [@\ 5a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"\ 6lt_mod_m_m\ 5/a\ 6 //] >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"\ 6distributive_times_plus_r\ 5/a\ 6
+   >\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 //
   ]
 qed.
 
-theorem divides_to_congruent: ∀n,m,p:nat. O < p → m ≤ n → 
-  p ∣(n - m) → n ≅_{p} m .
+theorem divides_to_congruent: ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 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 p → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → 
+  p \ 5a title="divides" href="cic:/fakeuri.def(1)"\ 6∣\ 5/a\ 6(n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 m) → n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6≅\ 5/a\ 6_{p} m .
 #n #m #p #posp #lemn * #l #eqpl 
-@(eq_times_plus_to_congruent … l posp) /2/
+@(\ 5a href="cic:/matita/arithmetics/congruence/eq_times_plus_to_congruent.def(14)"\ 6eq_times_plus_to_congruent\ 5/a\ 6 … l posp) /2/
 qed.
 
-theorem congruent_to_divides: ∀n,m,p:nat.O < p → 
-  n ≅_{p} m → p ∣ (n - m).
-#n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
->commutative_times >(div_mod n p) in ⊢ (??%?)
->(div_mod m p) in ⊢ (??%?) <(commutative_plus (m \mod p))
-<congnm <(minus_plus ? (n \mod p)) <minus_plus_m_m //
+theorem congruent_to_divides: ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 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 p → 
+  n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6≅\ 5/a\ 6_{p} m → p \ 5a title="divides" href="cic:/fakeuri.def(1)"\ 6∣\ 5/a\ 6 (n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 m).
+#n #m #p #posp #congnm @(\ 5a href="cic:/matita/arithmetics/primes/divides.con(0,1,2)"\ 6quotient\ 5/a\ 6 ? ? ((n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6(m \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)))
+>\ 5a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"\ 6commutative_times\ 5/a\ 6 >(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 n p) in ⊢ (??%?)
+>(\ 5a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"\ 6div_mod\ 5/a\ 6 m p) in ⊢ (??%?) <(\ 5a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"\ 6commutative_plus\ 5/a\ 6 (m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p))
+<congnm <(\ 5a href="cic:/matita/arithmetics/nat/minus_plus.def(12)"\ 6minus_plus\ 5/a\ 6 ? (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)) <\ 5a href="cic:/matita/arithmetics/nat/minus_plus_m_m.def(6)"\ 6minus_plus_m_m\ 5/a\ 6 //
 qed.
 
-theorem mod_times: ∀n,m,p:nat. O < p → 
-  n*m ≅_{p} (n \mod p)*(m \mod p).
-#n #m #p #posp @(eq_times_plus_to_congruent ?? p 
-  ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))) //
-@(trans_eq ?? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))))
-  [@eq_f2 //
-  |@(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
-    (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p))) //
-   >distributive_times_plus >distributive_times_plus_r 
-   >distributive_times_plus_r <associative_plus @eq_f2 //
+theorem mod_times: ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 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 p → 
+  n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6≅\ 5/a\ 6_{p} (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p).
+#n #m #p #posp @(\ 5a href="cic:/matita/arithmetics/congruence/eq_times_plus_to_congruent.def(14)"\ 6eq_times_plus_to_congruent\ 5/a\ 6 ?? p 
+  ((n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p))) //
+@(\ 5a href="cic:/matita/basics/logic/trans_eq.def(4)"\ 6trans_eq\ 5/a\ 6 ?? (((n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6((m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p))))
+  [@\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6 //
+  |@(\ 5a href="cic:/matita/basics/logic/trans_eq.def(4)"\ 6trans_eq\ 5/a\ 6 ? ? (((n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6((m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6
+    (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6((m \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p))) //
+   >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus.def(7)"\ 6distributive_times_plus\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"\ 6distributive_times_plus_r\ 5/a\ 6 
+   >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"\ 6distributive_times_plus_r\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6 //
   ]
 qed.
 
-theorem congruent_times: ∀n,m,n1,m1,p. O < p → 
-  n ≅_{p} n1 → m ≅_{p} m1 → n*m ≅_{p} n1*m1 .
+theorem congruent_times: ∀n,m,n1,m1,p. \ 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 p → 
+  n \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6≅\ 5/a\ 6_{p} n1 → m \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6≅\ 5/a\ 6_{p} m1 → n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6≅\ 5/a\ 6_{p} n1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m1 .
 #n #m #n1 #m1 #p #posp #congn #congm
-@(transitive_congruent … (mod_times n m p posp))
->congn >congm @sym_eq @mod_times //
+@(\ 5a href="cic:/matita/arithmetics/congruence/transitive_congruent.def(5)"\ 6transitive_congruent\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/congruence/mod_times.def(15)"\ 6mod_times\ 5/a\ 6 n m p posp))
+>congn >congm @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/congruence/mod_times.def(15)"\ 6mod_times\ 5/a\ 6 //
 qed.
 
 (*
@@ -115,4 +115,4 @@ apply congruent_times.
 assumption.
 apply congruent_n_mod_n.assumption.
 assumption.
-qed. *)
+qed. *)
\ No newline at end of file

diff --git a/weblib/arithmetics/factorial.ma b/weblib/arithmetics/factorial.ma
index fc7b7deeed5339c1a6e85dcc30c1911a26cb0213..006c4b964d2dbb762884dba9114ed74f273e20a5 100644 (file)
--- a/weblib/arithmetics/factorial.ma
+++ b/weblib/arithmetics/factorial.ma
@@ -13,72 +13,72 @@ include "arithmetics/exp.ma".
 
 let rec fact n ≝
   match n with 
-  [ O ⇒ 1
-  | S m ⇒ fact m * S m].
+  [ O ⇒ \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6
+  | 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].
 
 interpretation "factorial" 'fact n = (fact n).
 
-theorem le_1_fact : ∀n. 1 ≤ n!.
+theorem le_1_fact : ∀n. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 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.
 #n (elim n) normalize /2/ 
 qed.
 
-theorem le_2_fact : ∀n. 1 < n → 2 ≤ n!.
+theorem le_2_fact : ∀n. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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 '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.
 #n (cases n)
-  [#abs @False_ind /2/
-  |#m normalize #le2 @(le_times 1 ? 2) //
+  [#abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind /2/
+  |#m normalize #le2 @(\ 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6) //
   ]
 qed.
 
-theorem le_n_fact_n: ∀n. n ≤ n!.
+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.
 #n (elim n) normalize //
-#n #Hind @(transitive_le ? (1*(S n))) // @le_times //
+#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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 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 //
 qed.
 
-theorem lt_n_fact_n: ∀n. 2 < n → n < n!.
+theorem lt_n_fact_n: ∀n. \ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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 '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.
 #n (cases n) 
-  [#H @False_ind /2/ 
-  |#m #lt2 normalize @(lt_to_le_to_lt ? (2*(S m))) //
-   @le_times // @le_2_fact /2/ 
+  [#H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind /2/ 
+  |#m #lt2 normalize @(\ 5/a\ 6\ 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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 m))) //
+   @\ 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 /2/ 
 qed.
 
 (* approximations *)
 
-theorem fact_to_exp1: ∀n.O<n →
- (2*n)! ≤ (2^(pred (2*n))) * n! * n!.
-#n #posn (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H (elim posn) //
-#n #posn #Hind @(transitive_le ? ((2*n)!*(2*(S n))*(2*(S n))))
-  [>H normalize @le_times //
-  |cut (pred (2*(S n)) = S(S(pred(2*n))))
-    [>S_pred // @(le_times 1 ? 1) //] #H1
-   cut (2^(pred (2*(S n))) = 2^(pred(2*n))*2*2) 
+theorem fact_to_exp1: ∀n.\ 5/a\ 6\ 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 →
+ (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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="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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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 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.
+#n #posn (cut (∀i.\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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\ 6i)))) [//] #H (elim posn) //
+#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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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="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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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))))
+  [>H normalize @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times //
+  |cut (\ 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6) //] #H1
+   cut (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6) 
     [>H1 >H1 //] #H2 >H2
-   @(transitive_le ? ((2^(pred (2*n))) * n! * n! *(2*(S n))*(2*(S n))))
-    [@le_times[@le_times //]//
+   @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? ((\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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 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 //]//
     (* we generalize to hide the computational content *)
-    |normalize in match ((S n)!) generalize in match (S n)
-     #Sn generalize in match 2 #two //
+    |normalize in match ((\ 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) generalize in match (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)
+     #Sn generalize in match \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 #two //
     ]
   ]
 qed.  
 
 theorem fact_to_exp: ∀n.
- (2*n)! ≤ (2^(pred (2*n))) * n! * n!.
-#n (cases n) [normalize // |#n @fact_to_exp1 //]
+ (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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="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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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 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.
+#n (cases n) [normalize // |#n @\ 5a href="cic:/matita/arithmetics/factorial/fact_to_exp1.def(12)"\ 6fact_to_exp1 //]
 qed.
 
-theorem exp_to_fact1: ∀n.O < n →
-  2^(2*n)*n!*n! < (S(2*n))!.
+theorem exp_to_fact1: ∀n.\ 5/a\ 6\ 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 →
+  \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
 #n #posn (elim posn) [normalize //]
-#n #posn #Hind (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H
-cut (2^(2*(S n)) = 2^(2*n)*2*2) [>H //] #H1 >H1
-@(le_to_lt_to_lt ? (2^(2*n)*n!*n!*(2*(S n))*(2*(S n))))
-  [normalize in match ((S n)!) generalize in match (S n) #Sn
-   generalize in match 2 #two //
-  |cut ((S(2*(S n)))! = (S(2*n))!*(S(S(2*n)))*(S(S(S(2*n)))))
-   [>H //] #H2 >H2 @lt_to_le_to_lt_times
-     [@lt_to_le_to_lt_times //|>H // | //]
+#n #posn #Hind (cut (∀i.\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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\ 6i)))) [//] #H
+cut (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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
+@(\ 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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))))
+  [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
+   generalize in match \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 #two //
+  |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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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="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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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="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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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 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)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" 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)))))
+   [>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\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"\ 6lt_to_le_to_lt_times //|>H // | //]
   ]
-qed.
+qed.\ 5/a\ 6
      
 (* a slightly better result 
 theorem fact3: \forall n.O < n \to
@@ -193,4 +193,4 @@ intros.elim H
       ]
     ]
   ]
-qed. *)
+qed. *)
\ No newline at end of file

diff --git a/weblib/arithmetics/minimization.ma b/weblib/arithmetics/minimization.ma
index eda9d016618d1031be5b126b65b35ca105b9ee11..2959d0f3d1d14eb4b919dff3903d877f7047ce84 100644 (file)
--- a/weblib/arithmetics/minimization.ma
+++ b/weblib/arithmetics/minimization.ma
@@ -23,7 +23,7 @@ let rec max' i f d ≝
       
 definition max ≝ λn.λf.max' n f O.
 
-theorem max_O: ∀f. max O f = O.
+theorem max_O: ∀f. \ 5A href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/A\ 6 O f = O.
 // qed.
 
 theorem max_cases: ∀f.∀n.