proposition: Lemma Rplus_ge_reg_neg_r : forall r1 r2 r3, 0 >= r2 -> r1 + r2 >= r3 -> r1 >= r3.
proof: Proof. intros r1 r2 r3 H H'. apply (Rge_trans _ (r1 + r2)); try easy. now rewrite <-(Rplus_0_r r1) at 1; apply Rplus_ge_compat_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField