proposition: Lemma to_semiring_unique `{Naturals N} `{SemiRing SR} (f: N → SR) `{!SemiRing_Morphism f} x : f x = naturals_to_semiring N SR x.
proof: Proof. symmetry. pose proof (@semirings.mor_from_sr_to_alg _ _ _ (semirings.variety N) _ _ _ (semirings.variety SR) (λ _, f) _). set (@varieties.arrow semirings.theory _ _ _ (semirings.variety N) _ _ _ (semirings.variety SR) (λ _, f) _). apply (naturals_initial _ a 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