z := match z with | 0 => 0 | pos p => 1 | neg p => neg 1%pos end. Global Instance decpaths_binint : DecidablePaths BinInt. Proof. intros [n | | n] [m | | m]. + destruct (dec (n = m)) as [p | q]. - apply inl, ap, p. - by apply inr; intro; apply q, neg_inj. + exact (inr neg_neq_zero). + exact (inr neg_neq_pos). + exact (inr zero_neq_neg). + exact (inl idpath). + exact (inr zero_neq_pos). + exact (inr pos_neq_neg). + exact (inr pos_neq_zero). + destruct (dec (n = m)) as [p | q]. - apply inl, ap, p. - by apply inr; intro; apply q, pos_inj. Defined.
Require Import Basics. Require Import Spaces.Pos.Core.