proposition: Lemma Rplus_ge_compat : forall r1 r2 r3 r4, r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4.
proof: Proof. now intros r1 r2 r3 r4 H1%Rge_le H2%Rge_le; apply Rle_ge, Rplus_le_compat. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField