proposition: Lemma Rmult_Rdiv_lt_compat_l_rev: forall a b c : R, 0 < c -> a < b / c -> c * a < b.
proof: Proof. intros ; apply Rlt_le_trans with (c * (b / c))%R. apply Rmult_lt_compat_l ; assumption. right ; field ; apply Rgt_not_eq ; assumption. Qed.
imports: RIneq MyNeq Rfunctions Lra