proposition: Lemma id01_raw_help_le : forall (q:Qpos), ((1#2*id01_raw_help q) <= proj1_sig q)%Q.
proof: Proof. Proof with auto with *. intros q. unfold id01_raw_help, Qpos_ceiling. simpl. generalize (Qle_ceiling ((1#2)*/proj1_sig q)). generalize (Qceiling ((1#2)*/proj1_sig q)). intros [|p|p] H. elim (Qle_not_lt _ _ H). apply Q.Qmult_lt_0_compat... apply Qinv_lt_0_compat... autorewrite with QposElim in *. rewrite -> Qmake_Qdiv in *. rewrite Zpos_xO. rewrite -> Qle_minus_iff in *. change ((2%positive * p)%Z:Q) with (2%positive * p)%Q. replace RHS with (((2*proj1_sig q)/(2*p)) *(p - 1%positive/2%positive*/proj1_sig q))%Q. apply: mult_resp_nonneg; simpl; auto with *. apply Qlt_le_weak. apply Q.Qmult_lt_0_compat... simpl. field. split... elim (Qle_not_lt _ _ H). apply Qlt_trans with 0... apply Q.Qmult_lt_0_compat... apply Qinv_lt_0_compat... Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.metric2.IntegrableFunction CoRN.model.metric2.BoundedFunction CoRN.model.metric2.CRmetric CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.ftc.Integral CoRN.model.structures.StepQsec CoRN.model.structures.OpenUnit CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.L1metric CoRN.model.metric2.LinfMetric CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.model.metric2.Qmetric CoRN.reals.fast.ContinuousCorrect CoRN.ftc.IntegrationRules CoRN.ftc.MoreIntegrals CoRN.tactics.CornTac CoRN.model.metric2.LinfDistMonad