proposition: Lemma int_abs_0_alt x : int_abs Z N x = 0 ↔ x = 0.
proof: Proof. split; intros E1. destruct (int_abs_spec x) as [[_ E2]|[_ E2]]. now rewrite <-E2, E1, preserves_0. apply flip_negate_0. now rewrite <-E2, E1, preserves_0. rewrite E1, <-(preserves_0 (f:=f)). now apply int_abs_nat. 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