proposition: Lemma Cap_slow_help (f:Complete (X --> Y)) (x:Complete X) (e:Qpos) : ball (proj1_sig e) (Cap_slow_fun f x) (Cmap_slow (approximate f e) x).
proof: Proof. intros d1 d2. pose (exist (Qlt 0) (1#2) eq_refl) as half. set (d1' := (half * d1)%Qpos). set (f1 := (approximate f d1')). set (f2 := (approximate f e)). set (y1 := (Cmap_slow f1 x)). set (y2 := (Cmap_slow f2 x)). change (ball (proj1_sig d1 + proj1_sig e + proj1_sig d2) (approximate y1 d1') (approximate y2 (Qpos2QposInf d2))). setoid_replace (proj1_sig d1 + proj1_sig e + proj1_sig d2) with (proj1_sig (d1' + (d1' + e) + d2)%Qpos) by (simpl; ring). rewrite <- ball_Cunit. apply ball_triangle with y2;[|apply ball_approx_r]. apply ball_triangle with y1;[apply ball_approx_l|]. apply (uc_prf Cmap_strong_slow). apply (@regFun_prf _ (@ball (X-->Y))). Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax