proposition: Lemma to_semiring_involutive N `{Naturals N} N2 `{Naturals N2} x : naturals_to_semiring N2 N (naturals_to_semiring N N2 x) = x.
proof: Proof. rapply (proj2 (@categories.initials_unique' (varieties.Object semirings.theory) _ _ _ _ _ (semirings.object N) (semirings.object N2) _ naturals_initial _ naturals_initial) tt x). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.implementations.peano_naturals MathClasses.theory.rings Coq.Arith.PeanoNat MathClasses.categories.varieties MathClasses.theory.ua_transference MathClasses.interfaces.naturals