proposition: Lemma Rinv_le_contravar : forall x y, 0 < x -> x <= y -> / y <= / x.
proof: Proof. intros r1 r2 H1 [H2 | ->]. - now apply Rlt_le, Rinv_0_lt_contravar. - now apply Rle_refl. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField