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