commit by user utente

diff --git a/weblib/arithmetics/factorial.ma b/weblib/arithmetics/factorial.ma
index 006c4b964d2dbb762884dba9114ed74f273e20a5..e911a6fdb854e557e9eb267f8d0a31c56e36ab28 100644 (file)
--- 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 ⇒ \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6
+  [ O ⇒ \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6
   | S m ⇒ fact m \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m].
 
 interpretation "factorial" 'fact n = (fact n).
 
-theorem le_1_fact : ∀n. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
+theorem le_1_fact : ∀n. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
 #n (elim n) normalize /2/ 
 qed.
 
-theorem le_2_fact : ∀n. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
+theorem le_2_fact : ∀n. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
 #n (cases n)
-  [#abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind /2/
-  |#m normalize #le2 @(\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 ? \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6) //
+  [#abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/
+  |#m normalize #le2 @(\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 ? \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6) //
   ]
 qed.
 
 theorem le_n_fact_n: ∀n. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
 #n (elim n) normalize //
-#n #Hind @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))) // @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times //
+#n #Hind @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))) // @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 //
 qed.
 
-theorem lt_n_fact_n: ∀n. \ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
+theorem lt_n_fact_n: ∀n. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
 #n (cases n) 
-  [#H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind /2/ 
-  |#m #lt2 normalize @(\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m))) //
-   @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times // @\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/factorial/le_2_fact.def(12)"\ 6le_2_fact /2/ 
+  [#H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/ 
+  |#m #lt2 normalize @(\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt.def(4)"\ 6lt_to_le_to_lt\ 5/a\ 6 ? (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m))) //
+   @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 // @\ 5a href="cic:/matita/arithmetics/factorial/le_2_fact.def(12)"\ 6le_2_fact\ 5/a\ 6 /2/ 
 qed.
 
 (* approximations *)
 
-theorem fact_to_exp1: ∀n.\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6n →
- (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
-#n #posn (cut (∀i.\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6i)))) [//] #H (elim posn) //
-#n #posn #Hind @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? ((\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))))
-  [>H normalize @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times //
-  |cut (\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))))
-    [>\ 5a href="cic:/matita/arithmetics/nat/S_pred.def(3)"\ 6S_pred // @(\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 ? \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6) //] #H1
-   cut (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6) 
+theorem fact_to_exp1: ∀n.\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6n →
+ (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
+#n #posn (cut (∀i.\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6i)))) [//] #H (elim posn) //
+#n #posn #Hind @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? ((\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))))
+  [>H normalize @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 //
+  |cut (\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))))
+    [>\ 5a href="cic:/matita/arithmetics/nat/S_pred.def(3)"\ 6S_pred\ 5/a\ 6 // @(\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6 ? \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6) //] #H1
+   cut (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6) 
     [>H1 >H1 //] #H2 >H2
-   @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? ((\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))))
-    [@\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times[@\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times //]//
+   @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? ((\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))))
+    [@\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6[@\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 //]//
     (* we generalize to hide the computational content *)
-    |normalize in match ((\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6) generalize in match (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)
-     #Sn generalize in match \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 #two //
+    |normalize in match ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6) generalize in match (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)
+     #Sn generalize in match \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 #two //
     ]
   ]
 qed.  
 
 theorem fact_to_exp: ∀n.
- (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
-#n (cases n) [normalize // |#n @\ 5a href="cic:/matita/arithmetics/factorial/fact_to_exp1.def(12)"\ 6fact_to_exp1 //]
+ (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))) \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
+#n (cases n) [normalize // |#n @\ 5a href="cic:/matita/arithmetics/factorial/fact_to_exp1.def(12)"\ 6fact_to_exp1\ 5/a\ 6 //]
 qed.
 
-theorem exp_to_fact1: ∀n.\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n →
-  \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
+theorem exp_to_fact1: ∀n.\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n →
+  \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6.
 #n #posn (elim posn) [normalize //]
-#n #posn #Hind (cut (∀i.\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6i)))) [//] #H
-cut (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6) [>H //] #H1 >H1
-@(\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(5)"\ 6le_to_lt_to_lt\ 5/a\ 6 ? (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))))
+#n #posn #Hind (cut (∀i.\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6i)))) [//] #H
+cut (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6) [>H //] #H1 >H1
+@(\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(5)"\ 6le_to_lt_to_lt\ 5/a\ 6 ? (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural exponent" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n))))
   [normalize in match ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6) generalize in match (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) #Sn
-   generalize in match \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 #two //
-  |cut ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)))\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)))))
-   [>H //] #H2 >H2 @\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"\ 6lt_to_le_to_lt_times
-     [@\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"\ 6lt_to_le_to_lt_times //|>H // | //]
+   generalize in match \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6 #two //
+  |cut ((\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n)))\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n))\ 5a title="factorial" href="cic:/fakeuri.def(1)"\ 6!\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 62\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n)))))
+   [>H //] #H2 >H2 @\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"\ 6lt_to_le_to_lt_times\ 5/a\ 6
+     [@\ 5a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"\ 6lt_to_le_to_lt_times\ 5/a\ 6 //|>H // | //]
   ]
 qed.\ 5/a\ 6