proposition: Lemma opp_IZR : forall n:Z, IZR (- n) = - IZR n.
proof: Proof. intros [| p | p]; unfold IZR; simpl. - now replace R0 with 0 by reflexivity; rewrite Ropp_0. - reflexivity. - now rewrite Ropp_involutive. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField