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