proposition: Lemma IntervalOpenEta : forall {R : ConstructiveReals} (a b x : CRcarrier R), a < x < b -> { eta : CRcarrier R & prod (a < x-eta < x) (x < x+eta < b) }.
proof: Proof. intros. exists (CRmin (x-a) (b-x) * CR_of_Q R (1#2)). split. split. apply (CRplus_lt_reg_r (CRmin (x - a) (b - x) * CR_of_Q R (1 # 2))). apply (CRlt_le_trans _ x). 2: unfold CRminus; rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r; apply CRle_refl. apply (CRplus_lt_reg_l R (-a)). apply (CRle_lt_trans _ (CRmin (x - a) (b - x) * CR_of_Q R (1 # 2))). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. apply CRle_refl. apply (CRlt_le_trans _ (CRmin (x + - a) (b + - x) * 1)). 2: rewrite CRmult_1_r, CRplus_comm; apply CRmin_l. apply CRmult_lt_compat_l. apply CRmin_lt. apply CRlt_minus, (fst H). apply CRlt_minus, (snd H). apply CR_of_Q_lt. reflexivity. apply (CRlt_le_trans _ (x+0)). apply CRplus_lt_compat_l. rewrite <- CRopp_0. apply CRopp_gt_lt_contravar. apply CRmult_lt_0_compat. apply CRmin_lt. apply CRlt_minus. exact (fst H). apply CRlt_minus. exact (snd H). apply CR_of_Q_pos. reflexivity. rewrite CRplus_0_r. apply CRle_refl. split. apply (CRle_lt_trans _ (x+0)). rewrite CRplus_0_r. apply CRle_refl. apply CRplus_lt_compat_l. apply CRmult_lt_0_compat. apply CRmin_lt. apply CRlt_minus. exact (fst H). apply CRlt_minus. exact (snd H). apply CR_of_Q_pos. reflexivity. apply (CRplus_lt_reg_l R (-x)). apply (CRle_lt_trans _ (CRmin (x - a) (b - x) * CR_of_Q R (1 # 2))). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. apply CRle_refl. apply (CRle_lt_trans _ ((b - x) * CR_of_Q R (1 # 2))). apply CRmult_le_compat_r. apply CR_of_Q_le. discriminate. apply CRmin_r. apply (CRlt_le_trans _ ((b-x)*CR_of_Q _ 1)). apply CRmult_lt_compat_l. apply CRlt_minus. exact (snd H). apply CR_of_Q_lt. reflexivity. rewrite CRplus_comm, <- (CRmult_1_r (b + - x)). apply CRle_refl. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia