proposition: Lemma Rlt_plus_1 : forall r, r < r + 1.
proof: Proof. intros r; rewrite <-(Rplus_0_r r) at 1; apply Rplus_le_lt_compat. - now apply Rle_refl. - exact Rlt_0_1. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField