proposition: Lemma Rmult_Rinv_lt_compat_l : forall a b c, 0 < c -> a < b * c -> a * / c < b.
proof: Proof. intros a b c a_pos Habc ; apply Rlt_le_trans with (b * c * / c). apply Rmult_lt_compat_r ; [apply Rinv_0_lt_compat |] ; assumption. right ; field ; apply Rgt_not_eq ; assumption. Qed.
imports: RIneq MyNeq Rfunctions Lra