intros.reflexivity.
qed.
-alias num (instance 0) = "natural number".
-lemma times_SSO: \forall n.2*(S n) = S(S(2*n)).
-intro.simplify.rewrite < plus_n_Sm.reflexivity.
-qed.
-
theorem lt_O_to_fact1: \forall n.O<n \to
fact (2*n) \le (exp 2 (pred (2*n)))*(fact n)*(fact n).
intros.elim H