a b : n_to_z a * n_to_z b = 0 -> n_to_z a = 0 |_| n_to_z b = 0. Proof. rewrite <-rings.preserves_mult. rewrite <-!(naturals.to_semiring_unique (cast N Z)). intros E. change 0 with (' 0) in E. apply (injective _) in E. apply zero_product in E. destruct E as [E|E];rewrite E;[left|right];apply preserves_0. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.