proposition: Lemma Rinv_lt_0_contravar : forall r1 r2, r2 < 0 -> r1 < r2 -> / r2 < / r1.
proof: Proof. intros r1 r2 H2%Ropp_lt_contravar I%Ropp_lt_contravar. apply Ropp_lt_cancel. rewrite Ropp_0 in H2. now rewrite <-2(Rinv_opp); apply Rinv_0_lt_contravar. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField