proposition: Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2.
proof: Proof. now intros r1 r2 [I | ->]; [left | right; easy]; apply Ropp_lt_contravar. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField