proposition: Lemma Rplus_pos_nneg : 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_gt_ge_compat. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField