proposition: Lemma MonadLaw1 : forall a, Cmap_slow_fun (uc_id X) a =m a.
proof: Proof. intros x e1 e2. rewrite Qplus_0_r. simpl. eapply ball_weak_le; [|apply regFun_prf]. simpl. apply Qplus_le_l. rewrite <- (Qmult_1_l (proj1_sig e1)), Qmult_assoc. apply Qmult_le_r. apply Qpos_ispos. discriminate. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax