proposition: Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2.
proof: Proof. now intros r1 r2 I%Ropp_lt_contravar; rewrite 2Ropp_involutive in I. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField