proposition: Lemma UC_plus : forall {R : ConstructiveReals} (f g : CRcarrier R -> CRcarrier R) (modF modG : forall x:CRcarrier R, 0 < x -> CRcarrier R), UniformCont f modF -> UniformCont g modG -> UniformCont (fun x:CRcarrier R => f x + g x) (fun eps epsPos => CRmin (modF (eps * CR_of_Q R (1#2)) (eps2_Rgt_R0 eps epsPos)) (modG (eps * CR_of_Q R (1#2)) (eps2_Rgt_R0 eps epsPos))).
proof: Proof. split. - intros. apply CRmin_lt. destruct H. apply c. destruct H0. apply c. - intros. setoid_replace (f x + g x - (f y + g y)) with (f x - f y + (g x - g y)). apply (CRle_lt_trans _ _ _ (CRabs_triang _ _)). setoid_replace eps with (eps* CR_of_Q R (1#2) + eps* CR_of_Q R (1#2)). apply CRplus_le_lt_compat. apply CRlt_asym. destruct H. apply (c0 _ _ _ (eps2_Rgt_R0 eps epsPos)). apply (CRlt_le_trans _ (CRmin (modF (eps * CR_of_Q R (1#2)) (eps2_Rgt_R0 eps epsPos)) (modG (eps * CR_of_Q R (1#2)) (eps2_Rgt_R0 eps epsPos)))). apply H1. apply CRmin_l. destruct H0. apply (c0 _ _ _ (eps2_Rgt_R0 eps epsPos)). apply (CRlt_le_trans _ (CRmin (modF (eps * CR_of_Q R (1#2)) (eps2_Rgt_R0 eps epsPos)) (modG (eps * CR_of_Q R (1#2)) (eps2_Rgt_R0 eps epsPos)))). apply H1. apply CRmin_r. rewrite <- CRmult_plus_distr_l, <- CR_of_Q_plus. setoid_replace ((1 # 2) + (1#2))%Q with 1%Q. rewrite CRmult_1_r. reflexivity. reflexivity. unfold CRminus. do 2 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRplus_comm, CRopp_plus_distr. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRplus_comm. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal