proposition: Lemma from_nat_stmt (N':Type@{U}) `{Naturals@{U U U U U U U U} N'} : forall (P : SemiRings.Operations -> Type), P (SemiRings.BuildOperations N') -> P (SemiRings.BuildOperations N).
proof: Proof. apply SemiRings.iso_leibnitz with (naturals_to_semiring N' N);apply _. 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