proposition: Lemma Cjoin_prf : is_UniformlyContinuousFunction Cjoin_fun Qpos2QposInf.
proof: Proof. intros e x y Hab d1 d2. do 2 rewrite <- ball_Cunit. setoid_replace (proj1_sig d1 + proj1_sig e + proj1_sig d2) with (proj1_sig (((1#2)*d1 + (1#2)*d1) + e + (((1#2)*d2) + (1#2)*d2)))%Qpos by (simpl; ring). apply ball_triangle with y. apply ball_triangle with x. apply ball_triangle with (Cunit (approximate x ((1#2) * d1)%Qpos)). rewrite -> ball_Cunit. refine (ball_approx_l _ _). apply ball_approx_l. assumption. eapply ball_triangle. apply ball_approx_r. rewrite -> ball_Cunit. refine (ball_approx_r _ _). Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax