proposition: Lemma same_morphism: z_to_r = f.
proof: Proof. intros [p n] z' E. rewrite <- E. clear E z'. rewrite SRpair_splits. preservation. rewrite 2!rings.preserves_negate. now rewrite 2!(naturals.to_semiring_twice _ _ _). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.categories MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.theory.jections MathClasses.implementations.semiring_pairs