proposition: Lemma eq_IZR : forall n m:Z, IZR n = IZR m -> n = m.
proof: Proof. intros n m H%(Rminus_diag_eq); rewrite Z_R_minus in H. now apply Zminus_eq, eq_IZR_R0. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField