proposition: Lemma plus_IZR : forall n m:Z, IZR (n + m) = IZR n + IZR m.
proof: Proof. intros [| p | p] [| q | q]; rewrite ?Rplus_0_l, ?Rplus_0_r, ?Z.add_0_l, ?Z.add_0_r; try easy. - now unfold IZR; simpl; apply plus_IPR. - now apply plus_IZR_NEG_POS. - now rewrite Rplus_comm, Z.add_comm; apply plus_IZR_NEG_POS. - now unfold IZR; simpl; rewrite plus_IPR, Ropp_plus_distr. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField