proposition: Lemma int_abs_unique (a b : IntAbs Z N) (z : Z) : int_abs Z N (ia:=a) z = int_abs Z N (ia:=b) z.
proof: Proof. unfold int_abs. destruct (int_abs_sig Z N (IntAbs:=a) z) as [[n1 E1]|[n1 E1]]; destruct (int_abs_sig Z N (IntAbs:=b) z) as [[n2 E2]|[n2 E2]]. - apply (injective (naturals_to_semiring N Z)). path_via z. - assert (E : n1 + n2 = 0);[|path_via 0;[|symmetry]; apply (naturals.zero_sum _ _ E)]. apply (injective (naturals_to_semiring N Z)). rewrite preserves_0,preserves_plus. rewrite E1,E2. apply plus_negate_r. - assert (E : n1 + n2 = 0);[|path_via 0;[|symmetry]; apply (naturals.zero_sum _ _ E)]. apply (injective (naturals_to_semiring N Z)). rewrite preserves_0,preserves_plus. rewrite E1,E2. apply plus_negate_l. - apply (injective (naturals_to_semiring N Z)). path_via (- z). Qed.
imports: HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.nat_int HoTT.Classes.theory.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.orders.rings