proposition: Lemma Z_abs_aux_neg@{} : forall a b z : N, a + z = b -> naturals_to_semiring N Z z = - ' {| PairT.pos := a; PairT.neg := b |}.
proof: 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.
imports: HoTT.HIT.quotient HoTT.TruncType HoTT.Basics.Trunc HoTT.Classes.implementations.peano_naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.interfaces.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.orders.sum HoTT.Classes.orders.rings HoTT.Classes.tactics.ring_tac HoTT.Classes.theory.naturals