proposition: Lemma Cmap_slow_fun_prf (x:Complete X) : is_RegularFunction (@ball Y) (Cmap_slow_raw x).
proof: Proof. intros e1 e2. unfold Cmap_slow_raw. cut (forall (e1 e2:Qpos), (QposInf_le (mu f e2) (mu f e1)) -> ball (m:=Y) (proj1_sig e1 + proj1_sig e2) (f (approximate x (QposInf_mult (Qpos2QposInf (1#2)) (QposInf_bind (mu f) e1)))) (f (approximate x (QposInf_mult (Qpos2QposInf (1#2)) (QposInf_bind (mu f) e2))))). intros H. assert (forall a b, {QposInf_le a b}+{QposInf_le b a}). intros [a|] [b|]; simpl; try tauto. apply Qle_total. destruct (H0 (mu f e2) (mu f e1)). auto. apply ball_sym. rewrite Qplus_comm. auto. clear e1 e2. intros e1 e2 H. apply ball_weak. apply Qpos_nonneg. apply ball_sym. simpl. apply Cmap_slow_raw_strong. simpl. destruct (mu f e1). simpl. destruct (mu f e2). simpl. apply Qmult_le_l. reflexivity. exact H. elim H. constructor. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax