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