proposition: Lemma Rmult_Rinv_le_compat_contravar : forall x y z, 0 < y -> x * / y <= z -> x <= y * z.
proof: Proof. intros x y z y_pos Hle. apply Rle_trans with (y * (x * / y)). right ; field ; apply Rgt_not_eq ; assumption. apply Rmult_le_compat_l ; [left |] ; assumption. Qed.
imports: RIneq MyNeq Rfunctions Lra