proposition: Lemma MonadLaw5 : forall a, (Cjoin_fun (X:=X) (Cunit_fun _ a)) =m a.
proof: Proof. intros x e1 e2. simpl. setoid_replace (proj1_sig e1+0+proj1_sig e2) with (proj1_sig ((1#2)*e1 + e2 + (1#2)*e1)%Qpos) by (simpl; ring). apply ball_weak. apply Qpos_nonneg. apply regFun_prf. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax