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