proposition: Lemma ROpenBallConvex : forall {R : ConstructiveReals} (x r a b c : CRcarrier R), (a <= b /\ b <= c) -> CRabs _ (x - a) <= r -> CRabs _ (x - c) <= r -> CRabs _ (x - b) <= r.
proof: Proof. intros. apply CRabs_le. destruct H. apply CRabs_def2 in H0. apply CRabs_def2 in H1. split. - apply (CRle_trans _ (x-c)). apply H1. apply CRplus_le_compat_l. apply CRopp_ge_le_contravar. apply H2. - apply (CRle_trans _ (x-a)). 2: apply H0. apply CRplus_le_compat_l. apply CRopp_ge_le_contravar. apply H. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits