proposition: Lemma Cap_slow_prf : is_UniformlyContinuousFunction Cap_weak_slow Qpos2QposInf.
proof: Proof. intros e f1 f2 H. split. apply Qpos_nonneg. intro x. apply ball_closed. intros d dpos. setoid_replace (proj1_sig e + d) with (proj1_sig ((1#4)*exist _ _ dpos + ((1#4)*exist _ _ dpos + e + (1#4)*exist _ _ dpos) + (1#4)*exist _ _ dpos)%Qpos) by (simpl; ring). apply ball_triangle with (Cmap_strong_slow (approximate f2 ((1#4)*exist _ _ dpos)%Qpos) x). apply ball_triangle with (Cmap_strong_slow (approximate f1 ((1#4)*exist _ _ dpos)%Qpos) x). apply Cap_slow_help. apply (uc_prf Cmap_strong_slow). 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