proposition: Lemma EnlargePointMajorationZero : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (x : CRcarrier R) (modF : forall x:CRcarrier R, 0 < x -> CRcarrier R), UniformCont f modF -> 0 < f x -> { eta : CRcarrier R & prod (0 < eta) (forall y:CRcarrier R, CRabs _ (x-y) < eta -> 0 < (f y)) }.
proof: Proof. intros. destruct H as [H H1]. exists (modF (f x) H0). split. - apply H. - intros. specialize (H1 (f x) x y H0 H2). apply (CRle_lt_trans _ _ _ (CRle_abs _)) in H1. apply (CRplus_lt_reg_l _ (f x - f y)). rewrite CRplus_0_r. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. exact H1. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal