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]];[|apply flip_negate_0]; rewrite <-E2, E1, (preserves_0 (f:=f)); trivial. - rewrite E1, <-(preserves_0 (f:=f)). apply int_abs_nat. 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