Z_to_ring_morphism@{} `{IsCRing B} : IsSemiRingPreserving (integers_to_ring Z B) := ltac:(first [exact Z_to_ring_morphism'@{Ularge}| exact Z_to_ring_morphism'@{}]).
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.