proposition: Lemma to_semiring_injective `{Naturals N} `{IsSemiRing A} (f: A -> N) (g: N -> A) `{!IsSemiRingPreserving f} `{!IsSemiRingPreserving g} : IsInjective g.
proof: 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.
imports: HoTT.Basics.Decidable HoTT.Classes.interfaces.orders HoTT.Classes.implementations.peano_naturals HoTT.Classes.theory.rings HoTT.Classes.isomorphisms.rings HoTT.Classes.interfaces.naturals