proposition: Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.
proof: Proof. intros z1 z2 H; apply Z.lt_0_sub. apply lt_0_IZR. rewrite <- Z_R_minus. exact (Rgt_minus (IZR z2) (IZR z1) H). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField