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