X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Farithmetics%2Ffactorial.ma;h=eb5208017711ebd5f1f8078ee59a1518f0e90cb2;hb=829e3a8af3229c4e625245f7265dd67939da98c4;hp=006c4b964d2dbb762884dba9114ed74f273e20a5;hpb=e7993cbfabd54c9ced3b13a4d0ec418984ce5d1f;p=helm.git

diff --git a/weblib/arithmetics/factorial.ma b/weblib/arithmetics/factorial.ma
index 006c4b964..eb5208017 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
      
@@ -193,4 +193,6 @@ intros.elim H
       ]
     ]
   ]
-qed. *)
\ No newline at end of file
+qed. *)
+
+