-#n #posn #Hind (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H
-cut (2^(2*(S n)) = 2^(2*n)*2*2) [>H //] #H1 >H1
-@(le_to_lt_to_lt ? (2^(2*n)*n!*n!*(2*(S n))*(2*(S n))))
- [normalize in match ((S n)!) generalize in match (S n) #Sn
- generalize in match 2 #two //
- |cut ((S(2*(S n)))! = (S(2*n))!*(S(S(2*n)))*(S(S(S(2*n)))))
- [>H //] #H2 >H2 @lt_to_le_to_lt_times
- [@lt_to_le_to_lt_times //|>H // | //]
+#n #posn #Hind (cut (∀i.\ 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)"\ 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 // | //]