proposition: Lemma Rmult_Rinv_le_compat : 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 * z * / y). apply Rmult_le_compat_r. left ; apply Rinv_0_lt_compat ; assumption. assumption. right ; field ; apply Rgt_not_eq ; assumption. Qed.
imports: RIneq MyNeq Rfunctions Lra