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