proposition: Lemma Rle_Rinv_pos : forall x y : R, (0 < x)%R -> (x <= y)%R -> (/y <= /x)%R.
proof: Proof. intros. apply Rle_Rinv. exact H. apply Rlt_le_trans with x ; assumption. exact H0. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)