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