proposition: Lemma int_abs_sig_alt x : (sig (fun n : N => f n = x)) |_| (sig (fun n : N => f n = - x)).
proof: Proof. destruct (int_abs_spec x) as [[??]|[??]]; eauto. 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