proposition: Lemma to_ring_twice `{Integers Z} `{Ring R1} `{Ring R2} (f : R1 → R2) (g : Z → R1) (h : Z → R2) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} `{!SemiRing_Morphism h} x : f (g x) = h x.
proof: Proof. now apply (to_ring_unique_alt (f ∘ g) h). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.implementations.natpair_integers MathClasses.interfaces.integers