proposition: Lemma to_ring_unique `{Integers Z} `{Ring R} (f: Z → R) {h: SemiRing_Morphism f} x : f x = integers_to_ring Z R x.
proof: Proof. symmetry. pose proof (rings.encode_morphism_and_ops (f:=f)). set (@varieties.arrow rings.theory _ _ _ (rings.encode_variety_and_ops _) _ _ _ (rings.encode_variety_and_ops _) (λ _, f) _). exact (integers_initial _ a tt x). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.implementations.natpair_integers MathClasses.interfaces.integers