proposition: Lemma Z_zero_product' : ZeroProduct Z.
proof: Proof. intros x y E. destruct (int_abs_sig Z N x) as [[a Ea]|[a Ea]], (int_abs_sig Z N y) as [[b Eb]|[b Eb]]. - rewrite <-Ea,<-Eb in E. apply zero_product_aux in E. rewrite <-Ea,<-Eb. trivial. - apply (ap negate) in E. rewrite negate_mult_distr_r in E. rewrite <-Ea,<-Eb in E. rewrite negate_0 in E. apply zero_product_aux in E. destruct E as [E|E]. + left;rewrite <-Ea;trivial. + right. apply (injective negate). rewrite negate_0,<-Eb;trivial. - apply (ap negate) in E. rewrite negate_mult_distr_l in E. rewrite <-Ea,<-Eb in E. rewrite negate_0 in E. apply zero_product_aux in E. destruct E as [E|E]. + left. apply (injective negate). rewrite negate_0,<-Ea;trivial. + right;rewrite <-Eb;trivial. - rewrite <-negate_mult_negate,<-Ea,<-Eb in E. apply zero_product_aux in E. destruct E as [E|E]. + left. apply (injective negate). rewrite negate_0,<-Ea;trivial. + right. apply (injective negate). rewrite negate_0,<-Eb;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