`{Naturals N} `{IsSemiCRing SR} (f: N -> SR) `{!IsSemiRingPreserving f} x : f x = naturals_to_semiring N SR x. Proof. symmetry. apply naturals_initial. Qed.
Require Import Require Import Import SemiRings.