`{Integers Z} `{IsCRing R1} `{IsCRing R2} (f : R1 -> R2) (g : Z -> R1) (h : Z -> R2) `{!IsSemiRingPreserving f} `{!IsSemiRingPreserving g} `{!IsSemiRingPreserving h} x : f (g x) = h x. Proof. exact (to_ring_unique_alt (f ∘ g) h _). Qed.
Require Import Require Import Import NatPair.Instances.