proposition: Lemma EnlargePointMajoration : forall {R : ConstructiveReals} (f g : CRcarrier R -> CRcarrier R) (x : CRcarrier R) (modF modG : forall x:CRcarrier R, 0 < x -> CRcarrier R), UniformCont f modF -> UniformCont g modG -> f x < g x -> { eta : CRcarrier R & prod (0 < eta) (forall y:CRcarrier R, CRabs _ (x-y) < eta -> f y < g y) }.
proof: Proof. intros. pose proof (UC_scale f modF (-(1)) H). pose proof (UC_plus (fun x => -(1)*f x) g _ modG H2 H0). destruct (EnlargePointMajorationZero (fun t => -(1)*f t + g t) x _ H3). rewrite <- CRopp_mult_distr_l, CRopp_mult_distr_r. rewrite CRmult_1_l. apply (CRplus_lt_reg_l _ (f x)). rewrite <- CRplus_assoc, CRplus_opp_r. rewrite CRplus_0_l, CRplus_0_r. exact H1. exists x0. destruct p. split. exact c. intros. specialize (c0 y H4). apply (CRplus_lt_compat_l _ (f y)) in c0. rewrite CRplus_0_r in c0. setoid_replace (g y) with (f y + (- (1) * f y + g y)). exact c0. rewrite <- CRopp_mult_distr_l, CRmult_1_l. rewrite <- CRplus_assoc, CRplus_opp_r. rewrite CRplus_0_l. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal