proposition: Lemma Z_to_ring_morphism' `{IsRing B} : IsSemiRingPreserving (integers_to_ring Z B).
proof: 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.
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