proposition: Lemma Rle_Rinv_neg : forall x y : R, (y < 0)%R -> (x <= y)%R -> (/y <= /x)%R.
proof: Proof. intros. apply Ropp_le_cancel. repeat rewrite Ropp_inv_permute. apply Rle_Rinv. auto with real. apply Rlt_le_trans with (Ropp y). auto with real. auto with real. auto with real. apply Rlt_dichotomy_converse. left. exact H. apply Rlt_dichotomy_converse. left. apply Rle_lt_trans with y ; assumption. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)