proposition: Lemma to_ring_involutive `{Integers Z} Z2 `{Integers Z2} x : integers_to_ring Z2 Z (integers_to_ring Z Z2 x) = x.
proof: Proof. rapply (proj2 (@categories.initials_unique' _ _ _ _ _ _ (rings.object Z) (rings.object Z2) _ integers_initial _ integers_initial) tt x). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.implementations.natpair_integers MathClasses.interfaces.integers