proposition: Lemma Abs_Integral : forall x, (Qabs (IntegralQ x) <= IntegralQ (QabsS ^@> x))%Q.
proof: Proof. intros x. induction x. apply Qle_refl. rewriteStepF. eapply Qle_trans. apply Qabs_triangle. do 2 rewrite -> Qabs_Qmult. rewrite -> (Qabs_pos o); auto with *. rewrite -> (Qabs_pos (1-o)); auto with *. apply: plus_resp_leEq_both;simpl; apply: mult_resp_leEq_lft; simpl; auto with *. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.structures.StepQsec CoRN.metric2.UniformContinuity CoRN.metric2.Prelength CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.algebra.COrdFields2 CoRN.tactics.CornTac