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