From: Wilmer Ricciotti Date: Mon, 5 Sep 2011 11:28:56 +0000 (+0000) Subject: commit by user utente X-Git-Tag: make_still_working~2321 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e7993cbfabd54c9ced3b13a4d0ec418984ce5d1f;p=helm.git commit by user utente --- diff --git a/weblib/arithmetics/congruence.ma b/weblib/arithmetics/congruence.ma index d1afc19ee..6217aa57c 100644 --- 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: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a ≝ +λn,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a n. -definition congruent: nat → nat → nat → Prop ≝ -λn,m,p:nat. mod n p = mod m p. +definition congruent: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ +λn,m,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"mod/a n p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"mod/a 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:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} n . // qed. theorem transitive_congruent: - ∀p.transitive nat (λn,m.congruent n m p). + ∀p.a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (λn,m.a href="cic:/matita/arithmetics/congruence/congruent.def(4)"congruent/a 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:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m. +#n #m #ltnm @(a href="cic:/matita/arithmetics/div_and_mod/div_mod_spec_to_eq2.def(10)"div_mod_spec_to_eq2/a n m a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a n (na title="natural divide" href="cic:/fakeuri.def(1)"//am) (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a m)) +% // @a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a @(a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(6)"ltn_to_ltO/a … ltnm) qed. -theorem mod_mod : ∀n,p:nat. O

(div_mod (n \mod p) p) in ⊢ (? ? % ?) ->(eq_div_O ? p) // @lt_mod_m_m // +theorem mod_mod : ∀n,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural 'less than'" href="cic:/fakeuri.def(1)"</ap → n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p) a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p. +#n #p #posp >(a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p) p) in ⊢ (? ? % ?) +>(a href="cic:/matita/arithmetics/div_and_mod/eq_div_O.def(14)"eq_div_O/a ? p) // @a href="cic:/matita/arithmetics/div_and_mod/lt_mod_m_m.def(12)"lt_mod_m_m/a // qed. -theorem mod_times_mod : ∀n,m,p:nat. O

distributive_times_plus_r - >associative_plus associative_times a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"distributive_times_plus_r/a + >a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a <a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a >a href="cic:/matita/arithmetics/nat/associative_times.def(10)"associative_times/a <a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a // ] qed. -theorem congruent_n_mod_n : ∀n,p:nat. O < p → - n ≅_{p} (n \mod p). +theorem congruent_n_mod_n : ∀n,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → + n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a 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:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → + n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} (n a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a (ma title="natural times" href="cic:/fakeuri.def(1)"*/ap)). /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:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → + n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ra title="natural times" href="cic:/fakeuri.def(1)"*/apa title="natural plus" href="cic:/fakeuri.def(1)"+/am → n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{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 a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"distributive_times_plus_r/a + >a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a <a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a // ] 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:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → + p a title="divides" href="cic:/fakeuri.def(1)"∣/a(n a title="natural minus" href="cic:/fakeuri.def(1)"-/a m) → n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} m . #n #m #p #posp #lemn * #l #eqpl -@(eq_times_plus_to_congruent … l posp) /2/ +@(a href="cic:/matita/arithmetics/congruence/eq_times_plus_to_congruent.def(14)"eq_times_plus_to_congruent/a … 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)) -a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"commutative_times/a >(a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a n p) in ⊢ (??%?) +>(a href="cic:/matita/arithmetics/div_and_mod/div_mod.def(9)"div_mod/a m p) in ⊢ (??%?) <(a href="cic:/matita/arithmetics/nat/commutative_plus.def(5)"commutative_plus/a (m a title="natural remainder" href="cic:/fakeuri.def(1)"\mod/a p)) +distributive_times_plus >distributive_times_plus_r - >distributive_times_plus_r a href="cic:/matita/arithmetics/nat/distributive_times_plus.def(7)"distributive_times_plus/a >a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"distributive_times_plus_r/a + >a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"distributive_times_plus_r/a <a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a @a href="cic:/matita/basics/logic/eq_f2.def(3)"eq_f2/a // ] 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. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p → + n a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} n1 → m a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} m1 → na title="natural times" href="cic:/fakeuri.def(1)"*/am a title="congruent" href="cic:/fakeuri.def(1)"≅/a_{p} n1a title="natural times" href="cic:/fakeuri.def(1)"*/am1 . #n #m #n1 #m1 #p #posp #congn #congm -@(transitive_congruent … (mod_times n m p posp)) ->congn >congm @sym_eq @mod_times // +@(a href="cic:/matita/arithmetics/congruence/transitive_congruent.def(5)"transitive_congruent/a … (a href="cic:/matita/arithmetics/congruence/mod_times.def(15)"mod_times/a n m p posp)) +>congn >congm @a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a @a href="cic:/matita/arithmetics/congruence/mod_times.def(15)"mod_times/a // 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 fc7b7deee..006c4b964 100644 --- 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 ⇒ a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"1/a + | S m ⇒ fact m a title="natural times" href="cic:/fakeuri.def(1)"*/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m]. interpretation "factorial" 'fact n = (fact n). -theorem le_1_fact : ∀n. 1 ≤ n!. +theorem le_1_fact : ∀n. a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"1/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a na title="factorial" href="cic:/fakeuri.def(1)"!/a. #n (elim n) normalize /2/ qed. -theorem le_2_fact : ∀n. 1 < n → 2 ≤ n!. +theorem le_2_fact : ∀n. a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"1/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a na title="factorial" href="cic:/fakeuri.def(1)"!/a. #n (cases n) - [#abs @False_ind /2/ - |#m normalize #le2 @(le_times 1 ? 2) // + [#abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind /2/ + |#m normalize #le2 @(/aa href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"1/a ? a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/a) // ] qed. -theorem le_n_fact_n: ∀n. n ≤ n!. +theorem le_n_fact_n: ∀n. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a na title="factorial" href="cic:/fakeuri.def(1)"!/a. #n (elim n) normalize // -#n #Hind @(transitive_le ? (1*(S n))) // @le_times // +#n #Hind @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"1/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n))) // @a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times // qed. -theorem lt_n_fact_n: ∀n. 2 < n → n < n!. +theorem lt_n_fact_n: ∀n. /aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a na title="factorial" href="cic:/fakeuri.def(1)"!/a. #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 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind /2/ + |#m #lt2 normalize @(/aa href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"lt_to_le_to_lt/a ? (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m))) // + @a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times // @/aa href="cic:/matita/arithmetics/factorial/le_2_fact.def(12)"le_2_fact /2/ qed. (* approximations *) -theorem fact_to_exp1: ∀n.OH 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./aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural 'less than'" href="cic:/fakeuri.def(1)"</an → + (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an)a title="factorial" href="cic:/fakeuri.def(1)"!/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural exponent" href="cic:/fakeuri.def(1)"^/a(a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an))) a title="natural times" href="cic:/fakeuri.def(1)"*/a na title="factorial" href="cic:/fakeuri.def(1)"!/a a title="natural times" href="cic:/fakeuri.def(1)"*/a na title="factorial" href="cic:/fakeuri.def(1)"!/a. +#n #posn (cut (∀i.a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/ai)))) [//] #H (elim posn) // +#n #posn #Hind @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? ((a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an)a title="factorial" href="cic:/fakeuri.def(1)"!/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n))a title="natural times" href="cic:/fakeuri.def(1)"*/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)))) + [>H normalize @a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times // + |cut (/aa href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an)))) + [>a href="cic:/matita/arithmetics/nat/S_pred.def(3)"S_pred // @(/aa href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"1/a ? a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"1/a) //] #H1 + cut (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural exponent" href="cic:/fakeuri.def(1)"^/a(a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n))) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural exponent" href="cic:/fakeuri.def(1)"^/a(a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an))a title="natural times" href="cic:/fakeuri.def(1)"*/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/a) [>H1 >H1 //] #H2 >H2 - @(transitive_le ? ((2^(pred (2*n))) * n! * n! *(2*(S n))*(2*(S n)))) - [@le_times[@le_times //]// + @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? ((a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural exponent" href="cic:/fakeuri.def(1)"^/a(a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an))) a title="natural times" href="cic:/fakeuri.def(1)"*/a na title="factorial" href="cic:/fakeuri.def(1)"!/a a title="natural times" href="cic:/fakeuri.def(1)"*/a na title="factorial" href="cic:/fakeuri.def(1)"!/a a title="natural times" href="cic:/fakeuri.def(1)"*/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n))a title="natural times" href="cic:/fakeuri.def(1)"*/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)))) + [@a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times[@/aa href="cic:/matita/arithmetics/nat/le_times.def(9)"le_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 ((/aa href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)a title="factorial" href="cic:/fakeuri.def(1)"!/a) generalize in match (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) + #Sn generalize in match a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/a #two // ] ] qed. theorem fact_to_exp: ∀n. - (2*n)! ≤ (2^(pred (2*n))) * n! * n!. -#n (cases n) [normalize // |#n @fact_to_exp1 //] + (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an)a title="factorial" href="cic:/fakeuri.def(1)"!/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural exponent" href="cic:/fakeuri.def(1)"^/a(a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an))) a title="natural times" href="cic:/fakeuri.def(1)"*/a na title="factorial" href="cic:/fakeuri.def(1)"!/a a title="natural times" href="cic:/fakeuri.def(1)"*/a na title="factorial" href="cic:/fakeuri.def(1)"!/a. +#n (cases n) [normalize // |#n @a href="cic:/matita/arithmetics/factorial/fact_to_exp1.def(12)"fact_to_exp1 //] qed. -theorem exp_to_fact1: ∀n.O < n → - 2^(2*n)*n!*n! < (S(2*n))!. +theorem exp_to_fact1: ∀n./aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → + a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural exponent" href="cic:/fakeuri.def(1)"^/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an)a title="natural times" href="cic:/fakeuri.def(1)"*/ana title="factorial" href="cic:/fakeuri.def(1)"!/aa title="natural times" href="cic:/fakeuri.def(1)"*/ana title="factorial" href="cic:/fakeuri.def(1)"!/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an))a title="factorial" href="cic:/fakeuri.def(1)"!/a. #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.a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/ai)))) [//] #H +cut (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural exponent" href="cic:/fakeuri.def(1)"^/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural exponent" href="cic:/fakeuri.def(1)"^/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an)a title="natural times" href="cic:/fakeuri.def(1)"*/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/a) [>H //] #H1 >H1 +@(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(5)"le_to_lt_to_lt/a ? (a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural exponent" href="cic:/fakeuri.def(1)"^/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an)a title="natural times" href="cic:/fakeuri.def(1)"*/ana title="factorial" href="cic:/fakeuri.def(1)"!/aa title="natural times" href="cic:/fakeuri.def(1)"*/ana title="factorial" href="cic:/fakeuri.def(1)"!/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n))a title="natural times" href="cic:/fakeuri.def(1)"*/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)))) + [normalize in match ((a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)a title="factorial" href="cic:/fakeuri.def(1)"!/a) generalize in match (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) #Sn + generalize in match a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/a #two // + |cut ((a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n)))a title="factorial" href="cic:/fakeuri.def(1)"!/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an))a title="factorial" href="cic:/fakeuri.def(1)"!/aa title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an)))a title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(a title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"/aa title="natural number" href="cic:/fakeuri.def(1)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an))))) + [>H //] #H2 >H2 @a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"lt_to_le_to_lt_times + [@/aa href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"lt_to_le_to_lt_times //|>H // | //] ] -qed. +qed./a (* 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 eda9d0166..2959d0f3d 100644 --- 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. A href="cic:/matita/arithmetics/minimization/max.def(2)"max/A O f = O. // qed. theorem max_cases: ∀f.∀n.