proposition: Lemma Break_lt_3_eps : forall {R : ConstructiveReals} (a b : CRcarrier R), a < b -> { eps : CRcarrier R & prod (0 < eps) (a + CR_of_Q R 3 * eps < b) }.
proof: Proof. intros. exists ((b-a) * CR_of_Q R (1#4)). split. - rewrite <- (CRmult_0_l (CR_of_Q R (1#4))). apply CRmult_lt_compat_r. apply CR_of_Q_lt. reflexivity. rewrite <- (CRplus_opp_r a). apply CRplus_lt_compat_r. exact H. - rewrite (CRmult_comm (b-a)), <- CRmult_assoc, <- CR_of_Q_mult. apply (CRplus_lt_reg_l _ (-a)). rewrite <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l, (CRplus_comm (-a)). rewrite <- (CRmult_1_l (b + - a)). apply CRmult_lt_compat_r. rewrite <- (CRplus_opp_r a). apply CRplus_lt_compat_r. exact H. apply CR_of_Q_lt. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions