proposition: Lemma Rle_Rinv_neg : forall x y : R, (y < 0)%R -> (x <= y)%R -> (/y <= /x)%R.
proof: Proof. intros x y Hy H. apply Ropp_le_cancel. repeat rewrite Ropp_inv_permute. apply Rle_Rinv_pos. apply Ropp_0_gt_lt_contravar with (1 := Hy). apply Ropp_le_contravar with (1 := H). exact (Rlt_not_eq _ _ Hy). exact (Rlt_not_eq _ _ (Rle_lt_trans _ _ _ H Hy)). Qed.
imports: Reals