proposition: Lemma Qceiling_fact_le : forall q:Q, 0 < q -> q <= Pos.of_nat (fact (Pos.to_nat (Pos.succ (Z.to_pos (Z.log2_up (Qceiling q)))))) # 1.
proof: Proof. intros q H. apply (Qle_trans _ _ _ (Qle_ceiling q)). assert (0 < Qceiling q)%Z. { rewrite Zlt_Qlt. apply (Qlt_le_trans _ _ _ H). apply Qle_ceiling. } revert H0. generalize (Qceiling q). intros p ppos. clear H q. unfold Qle; simpl. rewrite Z.mul_1_r, Pos.mul_1_r. destruct p as [|p|p]. exfalso; inversion ppos. 2: exfalso; inversion ppos. clear ppos. apply (Z.le_trans _ (2 ^ Z.log2_up p)). apply Z.log2_up_le_pow2. reflexivity. apply Z.le_refl. revert p. apply Pos.peano_case. discriminate. intro p. generalize (Z.log2_up (Pos.succ p)) (Z.log2_up_pos (Pos.succ p) (Pos.lt_1_succ p)). clear p. intros p ppos. destruct p. inversion ppos. 2: inversion ppos. clear ppos. unfold Z.to_pos. pose proof (fact_power_2 (Pos.to_nat (Pos.succ p))). rewrite Pos2Nat.inj_succ in H. unfold pred in H. rewrite Pos2Nat.inj_succ. simpl (2^p)%Z. rewrite <- Pos2Z.inj_pow_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. 2: apply fact_neq_0. refine (Nat.le_trans _ _ _ _ H). clear H. generalize p. apply Pos.peano_ind. + apply Nat.le_refl. + intros. rewrite Pos2Nat.inj_succ, Pos.pow_succ_r. rewrite Pos2Nat.inj_mul. apply Nat.mul_le_mono_nonneg_l. apply Nat.le_0_l. exact H. 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