proposition: Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
proof: Proof. now intros r1 r2 I%Rge_le; apply Rge_le, Ropp_le_ge_contravar. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField