proposition: Lemma Rle_lt_0_plus_1 : forall r, 0 <= r -> 0 < r + 1.
proof: Proof. intros r H; apply Rlt_le_trans with (1 := Rlt_0_1). rewrite <-(Rplus_0_l 1) at 1. apply Rplus_le_compat; try easy. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField