proposition: Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n.
proof: Proof. induction n as [| [|n ] IHn]; intros H. - now inversion H. - now rewrite INR_1; apply Rlt_0_1. - rewrite S_INR; apply Rplus_lt_0_compat. + now apply IHn, Nat.lt_0_succ. + exact Rlt_0_1. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField