proposition: Lemma minus_IZR : forall n m:Z, IZR (n - m) = IZR n - IZR m.
proof: Proof. now intros n m; unfold Z.sub, Rminus; rewrite <-opp_IZR; apply plus_IZR. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField