proposition: Lemma Cjoin_fun_prf (x:Complete (Complete X)) : is_RegularFunction (@ball X) (Cjoin_raw x).
proof: Proof. intros d1 d2. rewrite <- ball_Cunit. setoid_replace (proj1_sig d1 + proj1_sig d2) with (proj1_sig ((1#2)*d1 + ((1#2)*d1+(1#2)*d2) + (1#2)*d2)%Qpos) by (simpl; ring). apply ball_triangle with (approximate x (Qpos_mult (exist (Qlt 0) (1#2) eq_refl) d2)). apply ball_triangle with (approximate x (Qpos_mult (exist (Qlt 0) (1#2) eq_refl) d1)). apply ball_approx_l. apply regFun_prf. apply ball_approx_r. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax