proposition: Lemma int_abs_unique_respectful {a b : IntAbs Z N} : ((=) ==> (=))%signature (int_abs Z N (ia:=a)) (int_abs Z N (ia:= b)).
proof: Proof. intros x y E. unfold int_abs, int_abs_sig. apply (injective (naturals_to_semiring N Z)). destruct a as [[z1 A]|[z1 A]], b as [[z2 B]|[z2 B]]. now rewrite A, B. symmetry. apply naturals.negate_to_ring. now rewrite A, B, involutive. apply naturals.negate_to_ring. now rewrite A, B, involutive. apply (injective (-)). now rewrite A, B, !involutive. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.nat_int MathClasses.theory.integers MathClasses.theory.rings MathClasses.orders.rings