proposition: Lemma fact_power_2 : forall n:nat, (2^pred n <= fact n)%nat.
proof: Proof. induction n. - apply Nat.le_refl. - apply (Nat.le_trans _ ((S n) * 2^pred n)). 2: apply Nat.mul_le_mono_nonneg_l; [apply Nat.le_0_l | exact IHn]. clear IHn. destruct n. simpl. apply Nat.le_refl. simpl. apply Nat.add_le_mono_l, Nat.add_le_mono_l, Nat.le_0_l. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.iso_CReals Coq.QArith.Qpower CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.transc.PowerSeries CoRN.reals.fast.CRpower CoRN.transc.Exponential CoRN.transc.RealPowers CoRN.reals.fast.Compress Coq.NArith.Ndigits CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.reals.fast.CRsign CoRN.reals.Q_in_CReals Coq.QArith.Qabs Coq.QArith.Qround CoRN.tactics.CornTac MathClasses.theory.int_pow MathClasses.interfaces.abstract_algebra