Z_abs_aux_0@{} : forall a b z : N, a + z = b -> z = 0 -> naturals_to_semiring N Z 0 = ' {| PairT.pos := a; PairT.neg := b |}. Proof. intros a b z E E'. rewrite (preserves_0 (A:=N)). rewrite E',plus_0_r in E. rewrite E. apply Z_path. red;simpl. apply plus_comm. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.