proposition: Lemma same_morphism: naturals_to_semiring N R ∘ f⁻¹ = h.
proof: Proof. intros x y F. rewrite <-F. transitivity ((h ∘ (f ∘ f⁻¹)) x). symmetry. apply (to_semiring_unique (h ∘ f)). unfold compose. now rewrite jections.surjective_applied. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.implementations.peano_naturals MathClasses.theory.rings Coq.Arith.PeanoNat MathClasses.categories.varieties MathClasses.theory.ua_transference MathClasses.interfaces.naturals