proposition: Lemma toR_unique (h : nat -> R) `{!IsSemiRingPreserving h} x : naturals_to_semiring nat R x = h x.
proof: Proof. induction x as [|n E]. + change (0 = h 0). apply symmetry,preserves_0. + rewrite f_S. change (1 + naturals_to_semiring nat R n = h (1+n)). rewrite (preserves_plus (f:=h)). rewrite E. apply ap10,ap,symmetry,preserves_1. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.semirings HoTT.Classes.theory.apartness