`{Naturals N} `{IsSemiCRing A} (f: A -> N) (g: N -> A) `{!IsSemiRingPreserving f} `{!IsSemiRingPreserving g} : IsInjective g. Proof. intros x y E. change (id x = id y). rewrite <-(to_semiring_twice f g id x), <-(to_semiring_twice f g id y). apply ap,E. Qed.
Require Import Require Import Import SemiRings.