Z_abs_def@{} : forall x : PairT.T N, (exists n : N, naturals_to_semiring N Z n = ' x) |_| (exists n : N, naturals_to_semiring N Z n = - ' x). Proof. intros [a b]. destruct (nat_distance_sig a b) as [[z E]|[z E]]. - destruct (dec (z = 0)) as [E'|_]. + left. exists 0. apply Z_abs_aux_0 with z;trivial. + right. exists z. apply Z_abs_aux_neg;trivial. - left. exists z. apply Z_abs_aux_pos;trivial. Defined.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.