proposition: Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
proof: Proof. intros r1 r2 H. apply (Rplus_lt_reg_l r1), (Rplus_lt_reg_r r2). now rewrite Rplus_opp_r, Rplus_0_l, Rplus_assoc, Rplus_opp_l, Rplus_0_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField