From 572f5e918cd2c81ed3844714d647ad1a30cc7547 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 5 Sep 2011 11:48:38 +0000 Subject: [PATCH] commit by user utente --- weblib/arithmetics/factorial.ma | 66 ++++++++++++++++----------------- 1 file changed, 33 insertions(+), 33 deletions(-) diff --git a/weblib/arithmetics/factorial.ma b/weblib/arithmetics/factorial.ma index 006c4b964..e911a6fdb 100644 --- a/weblib/arithmetics/factorial.ma +++ b/weblib/arithmetics/factorial.ma @@ -13,70 +13,70 @@ include "arithmetics/exp.ma". let rec fact n ≝ match n with - [ 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 + [ O ⇒ a 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. 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. +theorem le_1_fact : ∀n. a 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. 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. +theorem le_2_fact : ∀n. a 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)"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 @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) // + [#abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ + |#m normalize #le2 @(a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a a title="natural number" href="cic:/fakeuri.def(1)"1/a ? a title="natural number" href="cic:/fakeuri.def(1)"2/a) // ] qed. 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 @(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 // +#n #Hind @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (a 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/a // qed. -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. +theorem lt_n_fact_n: ∀n. a 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 @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/ + [#H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ + |#m #lt2 normalize @(a 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)"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/a // @a href="cic:/matita/arithmetics/factorial/le_2_fact.def(12)"le_2_fact/a /2/ qed. (* approximations *) -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) +theorem fact_to_exp1: ∀n.a 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)"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)"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)"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)"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)"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)"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)"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)"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/a // + |cut (a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a 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)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/an)))) + [>a href="cic:/matita/arithmetics/nat/S_pred.def(3)"S_pred/a // @(a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a a title="natural number" href="cic:/fakeuri.def(1)"1/a ? a title="natural number" href="cic:/fakeuri.def(1)"1/a) //] #H1 + cut (a 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)"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)"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)"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)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/aa title="natural number" href="cic:/fakeuri.def(1)"2/a) [>H1 >H1 //] #H2 >H2 - @(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 //]// + @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? ((a 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)"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)"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)"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/a[@a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a //]// (* we generalize to hide the computational content *) - |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 // + |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)"2/a #two // ] ] qed. theorem fact_to_exp: ∀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 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 //] + (a 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)"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)"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/a //] qed. -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. +theorem exp_to_fact1: ∀n.a 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)"2/aa title="natural exponent" href="cic:/fakeuri.def(1)"^/a(a 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)"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.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)))) +#n #posn #Hind (cut (∀i.a 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)"2/aa title="natural times" href="cic:/fakeuri.def(1)"*/ai)))) [//] #H +cut (a 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)"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)"2/aa title="natural exponent" href="cic:/fakeuri.def(1)"^/a(a 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)"2/aa title="natural times" 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)"2/aa title="natural exponent" href="cic:/fakeuri.def(1)"^/a(a 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)"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)"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 // | //] + generalize in match a 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)"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)"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)"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)"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/a + [@a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"lt_to_le_to_lt_times/a //|>H // | //] ] qed./a -- 2.39.2