proposition: Lemma Cap_weak_slow_prf (f:Complete (X --> Y)) : is_UniformlyContinuousFunction (Cap_slow_fun f) (Cap_slow_modulus f).
proof: Proof. intros e x y H. set (e' := ((1#3)*e)%Qpos). setoid_replace (proj1_sig e) with (proj1_sig (e'+e'+e')%Qpos) by (simpl; ring). apply ball_triangle with (Cmap_slow (approximate f e') y). apply ball_triangle with (Cmap_slow (approximate f e') x). apply Cap_slow_help. apply (uc_prf). apply H. apply ball_sym. apply Cap_slow_help. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax