proposition: Lemma Rinv_lt_contravar : forall r1 r2, 0 < r1 * r2 -> r1 < r2 -> / r2 < / r1.
proof: Proof. intros r1 r2 [[H1 H2] | [H1 H2]]%Rmult_pos_cases. - now apply Rinv_0_lt_contravar. - now apply Rinv_lt_0_contravar. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField