proposition: Lemma mul_factor_gt : forall eps l l':R, eps > 0 -> eps * mul_factor l l' > 0.
proof: Proof. intros; unfold Rgt; rewrite <- (Rmult_0_r eps); apply Rmult_lt_compat_l. - assumption. - unfold mul_factor; apply Rinv_0_lt_compat; cut (1 <= 1 + (Rabs l + Rabs l')). + cut (0 < 1). * exact (Rlt_le_trans _ _ _). * exact Rlt_0_1. + replace (1 <= 1 + (Rabs l + Rabs l')) with (1 + 0 <= 1 + (Rabs l + Rabs l')). * apply Rplus_le_compat_l. cut (Rabs (l + l') <= Rabs l + Rabs l'). -- cut (0 <= Rabs (l + l')). ++ exact (Rle_trans _ _ _). ++ exact (Rabs_pos _). -- exact (Rabs_triang _ _). * rewrite (proj1 (Rplus_ne 1)); trivial. Qed.
imports: Rbase Rfunctions Lra