Z_to_ring_morphism' `{IsCRing B} : IsSemiRingPreserving (integers_to_ring Z B). Proof. split;split;red. - change (@sg_op B _) with (@plus B _); change (@sg_op Z _) with (@plus Z _). apply (Z_ind2 _). intros [pa na] [pb nb]. unfold integers_to_ring;simpl. rewrite !(preserves_plus (f:=naturals_to_semiring N B)). rewrite negate_plus_distr. ring_with_nat. - change (@mon_unit B _) with (@zero B _); change (@mon_unit Z _) with (@zero Z _). unfold integers_to_ring;simpl. rewrite (preserves_0 (f:=naturals_to_semiring N B)). rewrite negate_0,plus_0_r;trivial. - change (@sg_op B _) with (@mult B _); change (@sg_op Z _) with (@mult Z _). apply (Z_ind2 _). intros [pa na] [pb nb]. unfold integers_to_ring;simpl. rewrite !(preserves_plus (f:=naturals_to_semiring N B)). rewrite !(preserves_mult (f:=naturals_to_semiring N B)). rewrite (preserves_plus (f:=naturals_to_semiring N B)). rewrite !(preserves_mult (f:=naturals_to_semiring N B)). rewrite negate_plus_distr. rewrite negate_mult_distr_r,negate_mult_distr_l. rewrite <-(negate_mult_negate (naturals_to_semiring N B na) (naturals_to_semiring N B nb)). ring_with_nat. - change (@mon_unit B _) with (@one B _); change (@mon_unit Z _) with (@one Z _). unfold integers_to_ring;simpl. rewrite (preserves_1 (f:=naturals_to_semiring N B)). rewrite (preserves_0 (f:=naturals_to_semiring N B)). rewrite negate_0,plus_0_r;trivial. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.