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