proposition: Lemma Rplus_ge_compat_r : forall r r1 r2, r1 >= r2 -> r1 + r >= r2 + r.
proof: Proof. now intros r r1 r2 H%Rge_le; apply Rle_ge, Rplus_le_compat_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField