proposition: Lemma plus_IZR_NEG_POS : forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q).
proof: Proof. unfold IZR; intros p q; simpl; rewrite Z.pos_sub_spec. destruct (Pos.compare_spec p q) as [-> | Lt | Gt]. - now rewrite Rplus_opp_r. - rewrite minus_IPR by (exact Lt); rewrite Ropp_minus_distr. now unfold Rminus; rewrite Rplus_comm. - now rewrite minus_IPR by (exact Gt); unfold Rminus. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField