proposition: Lemma Qclamp01_close : forall e x y, Qabs (x-y) <= e -> Qabs (Qclamp01 x - Qclamp01 y) <= e.
proof: Proof. intros e. cut (forall x y : Q, y <= x -> x - y <= e -> Qclamp01 x - Qclamp01 y <= e). intros H x y. destruct (Qle_total x y). rewrite -> Qabs_neg. intros He. rewrite -> Qabs_neg. replace LHS with (Qclamp01 y - Qclamp01 x) by simpl; ring. apply H; auto. replace LHS with (- (x-y)) by simpl; ring. auto. apply (shift_minus_leEq Q_as_COrdField). stepr (Qclamp01 y); [| now (simpl; ring)]. apply Qclamp01_le. auto. apply (shift_minus_leEq Q_as_COrdField). stepr y; [| now (simpl; ring)]. auto. rewrite -> Qabs_pos. intros He. rewrite -> Qabs_pos. apply H; auto. apply: shift_zero_leEq_minus. apply Qclamp01_le. auto. apply: shift_zero_leEq_minus. auto. intros x y Hxy He. simpl. apply (Qmin_case 1 y). intros Hy. assert (Hx:=Qle_trans _ _ _ Hy Hxy). rewrite -> Qle_min_l in Hx. rewrite -> Hx. replace LHS with 0 by simpl; ring. eapply Qle_trans;[|apply He]. apply: shift_zero_leEq_minus; auto. apply (Qmin_case 1 x). intros Hx Hy. eapply Qle_trans;[|apply He]. apply Qplus_le_compat; auto. apply Qopp_le_compat. apply Qmax_ub_r. intros _ _. apply (Qmax_case 0 x); intros Hx. assert (Hy:=Qle_trans _ _ _ Hxy Hx). rewrite -> Qle_max_l in Hy. rewrite -> Hy. eapply Qle_trans;[|apply He]. apply: shift_zero_leEq_minus; auto. apply (Qmax_case 0 y); intros Hy. eapply Qle_trans;[|apply He]. apply Qplus_le_compat; auto with *. auto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.algebra.Bernstein CoRN.algebra.CRing_Homomorphisms CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.model.totalorder.QMinMax CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.reals.fast.CRabs CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.CRArith CoRN.reals.fast.CRArith_alg