x : (naturals_to_semiring N R ∘ f^-1) x = h x. Proof. transitivity ((h ∘ (f ∘ f^-1)) x). - symmetry. apply (to_semiring_unique (h ∘ f)). - unfold Compose. apply ap, eisretr. Qed.
Require Import Require Import Import SemiRings.