proposition: Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0.
proof: Proof. unfold Rminus; intros r1 r2 H%(Rplus_ge_compat_r (-r2)). now rewrite Rplus_opp_r in H. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField