proposition: Lemma 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: 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.
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