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