proposition: Lemma is_UniformlyContinuousD : @is_UniformlyContinuousFunction Q_as_MetricSpace CR (fun x => g (clamp x)) (Qscale_modulus c).
proof: Proof. intros e a b Hab. assert (X:forall x, I (inj_Q _ (clamp x))). clear -I Hlr. intros x. destruct l; destruct r; try split; unfold clamp; apply: inj_Q_leEq; simpl; auto with *. assert (Y:=(fun a=> (Hg _ (Derivative_imp_inc _ _ _ _ Hf _ (X a)) (X a)))). do 2 rewrite -> Y. rewrite <- CRAbsSmall_ball. unfold cg_minus. simpl. stepl (IRasCR (inj_Q IR (proj1_sig e))); [| now simpl; apply IR_inj_Q_as_CR]. stepr (IRasCR ((f (inj_Q IR (clamp a)) (Derivative_imp_inc I properI f f' Hf (inj_Q IR (clamp a)) (X a)))[-] (f (inj_Q IR (clamp b)) (Derivative_imp_inc I properI f f' Hf (inj_Q IR (clamp b)) (X b))))) ; [| now simpl; apply IR_minus_as_CR]. rewrite <- IR_AbsSmall_as_CR. apply AbsIR_imp_AbsSmall. eapply leEq_transitive;[eapply Law_of_the_Mean_Abs_ineq;try apply Hf;try apply X|]. intros x H Hx. apply Hc. eapply included_interval;[| |apply H];apply X. revert Hab. apply Qscale_modulus_elim. intros Hc0 _. stepl (inj_Q IR (nring 0)). apply inj_Q_leEq. simpl; auto with *. setoid_replace (inj_Q IR c) with (inj_Q IR (nring 0)). rewrite -> inj_Q_nring. rational. apply inj_Q_wd. auto. intros y Hyc Hab. stepr ((inj_Q IR (proj1_sig e/proj1_sig y)%Q[*](inj_Q _ (proj1_sig y)))). apply mult_resp_leEq_both. eapply leEq_transitive. apply AbsIR_nonneg. apply (Hc _ (Derivative_imp_inc' I properI f f' Hf (inj_Q IR (clamp a)) (X a))). apply X. apply AbsIR_nonneg. apply inj_Q_leEq. destruct Hyc; auto. apply AbsSmall_imp_AbsIR. stepr (inj_Q IR (clamp a - clamp b)%Q); [| now apply inj_Q_minus]. apply inj_Q_AbsSmall. change (ball (proj1_sig y) (clamp a) (clamp b)). apply ball_clamp. auto. assert (Z:[0][<]inj_Q IR (proj1_sig y)). (stepl (inj_Q IR ([0]:Q)); [| now apply (inj_Q_nring IR 0)]); apply inj_Q_less; apply Qpos_ispos. eapply eq_transitive. apply mult_wdl. apply (inj_Q_div IR (proj1_sig e) _ (pos_ap_zero _ _ Z)). apply div_1. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.Q_in_CReals CoRN.reals.fast.CRIR CoRN.ftc.Rolle CoRN.tactics.CornTac CoRN.model.metric2.Qmetric CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax