proposition: Lemma MonadLaw7 : forall a, Cjoin_fun ((Cmap_slow_fun (X:=Complete (Complete X)) Cjoin) a) =m Cjoin_fun (Cjoin_fun a).
proof: Proof. intros x e1 e2. pose (half := fun e:Qpos => ((1#2)*e)%Qpos). apply ball_weak_le with (proj1_sig ((half (half e1)) + ((half (half e1)) + (half (half e1) + (half (half e2))) + (half (half e2))) + (half e2))%Qpos). unfold half. simpl. ring_simplify. apply Qplus_le_l. rewrite <- (Qmult_1_l (proj1_sig e1)) at 2. apply Qmult_le_r. apply Qpos_ispos. discriminate. apply (regFun_prf x). Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax