proposition: Lemma StrongMonadLaw1 : forall a b, msp_eq (Cap_slow_fun (Cunit_fun _ a) b) (Cmap_strong_slow a b).
proof: Proof. intros f x. apply regFunEq_equiv, regFunEq_e. intros e. apply ball_weak_le with (proj1_sig ((1#2)*e+e)%Qpos). simpl. rewrite -> Qle_minus_iff; ring_simplify. apply Qmult_le_0_compat. discriminate. apply Qpos_nonneg. refine (regFun_prf _ _ _). Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax