proposition: Lemma Rmult_continuous_zero {R : ConstructiveReals} (x eps : CRcarrier R) : 0 < eps -> { alpha : CRcarrier R & prod (0 < alpha) (alpha * x < eps) }.
proof: Proof. intros. destruct (CRltLinear R). destruct (s 0 x 1 (CRzero_lt_one R)). - assert (0 < x + 1). { apply (CRlt_trans _ (0 + 1)). rewrite CRplus_0_l. exact (CRzero_lt_one R). apply CRplus_lt_compat_r. exact c. } exists (eps * CRinv R (x+1) (inr H0)). split. apply CRmult_lt_0_compat. exact H. apply CRinv_0_lt_compat. exact H0. rewrite <- (CRmult_1_r eps). do 2 rewrite CRmult_assoc. apply CRmult_lt_compat_l. exact H. rewrite CRmult_1_l. apply (CRmult_lt_reg_l (x+1)). exact H0. rewrite <- CRmult_assoc, CRinv_r. rewrite CRmult_1_l, CRmult_1_r. rewrite <- (CRplus_0_r x), CRplus_assoc. apply CRplus_lt_compat_l. rewrite CRplus_0_l. exact (CRzero_lt_one R). - exists eps. split. exact H. rewrite <- (CRmult_1_r eps). rewrite CRmult_assoc. rewrite CRmult_1_l. exact (CRmult_lt_compat_l _ _ _ H c). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions