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