-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)