proposition: Lemma CunitCjoin : forall a, (Cunit_fun _ (Cjoin_fun (X:=X) a)) =m a.
proof: Proof. intros x e1 e2 d1 d2. rewrite Qplus_0_r. change (ball (proj1_sig d1 + (proj1_sig e1 + proj1_sig e2) + proj1_sig d2) (approximate (approximate x ((1#2) * d1)%Qpos) ((1#2) * d1)%Qpos) (approximate (approximate x e2) (Qpos2QposInf d2))). apply ball_weak_le with (proj1_sig (((1#2) * d1 + ((1#2) * d1 + e2) + d2))%Qpos). rewrite -> Qle_minus_iff. simpl. ring_simplify. auto with *. apply (regFun_prf x). Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax