proposition: Lemma to_semiring_self `{Naturals N} (f : N → N) `{!SemiRing_Morphism f} x : f x = x.
proof: Proof. now apply (to_semiring_unique_alt f id). 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