(a b : IntAbs Z N) (z : Z) : int_abs Z N (ia:=a) z = int_abs Z N (ia:=b) z. 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.
Require Import