proposition: Lemma MonadLaw2 : forall (f:Y --> Z) (g:X --> Y) a, Cmap_slow_fun (uc_compose f g) a =m (Cmap_slow_fun f (Cmap_slow_fun g a)).
proof: Proof. simpl. intros f g x e1 e2. rewrite Qplus_0_r. set (a := approximate (Cmap_slow_fun (uc_compose f g) x) e1). set (b:=(approximate (Cmap_slow_fun f (Cmap_slow_fun g x)) e2)). set (d0 := (QposInf_min (QposInf_mult (Qpos2QposInf (exist (Qlt 0) (1#2) eq_refl)) (mu (uc_compose f g) e1)) ((Qpos2QposInf (exist (Qlt 0) (1#2) eq_refl)) * QposInf_bind (mu g) (QposInf_mult (Qpos2QposInf (exist (Qlt 0) (1#2) eq_refl)) (mu f e2))))). apply ball_triangle with ((uc_compose f g) (approximate x d0)). apply ball_sym. apply Cmap_slow_raw_strong. unfold d0. apply QposInf_min_lb_l. unfold b; simpl. unfold Cmap_slow_raw. apply uc_prf. simpl. destruct (mu f e2) as [q|]; try constructor. simpl. apply ball_weak_le with (proj1_sig ((1#2)*q)%Qpos). simpl. rewrite <- (Qmult_1_l (proj1_sig q)) at 2. apply Qmult_le_r. apply Qpos_ispos. discriminate. apply (Cmap_slow_raw_strong g x d0). apply QposInf_min_lb_r. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax