proposition: Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z.
proof: Proof. intros n [H1 H2]; apply Z.le_antisymm. - now apply Z.lt_succ_r; apply lt_IZR. - replace 0%Z with (Z.succ (-1)) by reflexivity. now apply Z.le_succ_l, lt_IZR. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField