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