proposition: Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2.
proof: Proof. now intros r1 r2 I I'; rewrite <-(Rplus_0_r 0); apply Rplus_lt_le_compat. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField