proposition: Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.
proof: Proof. intros n m H; apply Rnot_le_lt; intros [I | E%eq_IZR]. - now apply (Z.lt_irrefl m), Z.lt_trans with (2 := H), lt_IZR. - now apply (Z.lt_irrefl m); rewrite E at 1. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField