Z_zero_product' : ZeroProduct Z. 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.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.