proposition: Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m.
proof: Proof. induction n as [| n IH]; intros m H. - now apply lt_0_INR. - destruct m as [| m']. + now apply Nat.nlt_0_r in H. + rewrite 2S_INR. now apply (Rplus_lt_compat_r 1), IH, Nat.succ_lt_mono. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField