proposition: Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
proof: Proof. intros n m. generalize dependent n. induction m as [| m IH]; intros n H. - now exfalso; apply Rlt_not_le with (1 := H), pos_INR. - destruct n as [| n]. + apply Nat.lt_0_succ. + apply ->Nat.succ_lt_mono; apply IH. rewrite 2!S_INR in H. now apply Rplus_lt_reg_r with (1 := H). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField