proposition: Lemma Z_to_ring_unique@{} `{IsRing B} (h : Z -> B) `{!IsSemiRingPreserving h} : forall x : Z, integers_to_ring Z B x = h x.
proof: Proof. pose proof Z_ring. apply (Z_ind _). intros [pa na];unfold integers_to_ring;simpl. rewrite Npair_splits. rewrite (preserves_plus (f:=h)),(preserves_negate (f:=h)). change (h (' pa)) with (Compose h (cast N Z) pa). change (h (' na)) with (Compose h (cast N Z) na). rewrite 2!(naturals_initial (h:=Compose h (cast N Z))). trivial. Qed.
imports: HoTT.HIT.quotient HoTT.TruncType HoTT.Basics.Trunc HoTT.Classes.implementations.peano_naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.interfaces.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.orders.sum HoTT.Classes.orders.rings HoTT.Classes.tactics.ring_tac HoTT.Classes.theory.naturals