proposition: Lemma MonadLaw6 : forall a, Cjoin_fun ((Cmap_slow_fun (X:=X) Cunit) a) =m a.
proof: Proof. intros a e1 e2. simpl. setoid_replace (proj1_sig e1 + 0 + proj1_sig e2) with (proj1_sig ((1#2)*((1#2)*e1) + e2 + (3#4)*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