proposition: Theorem eq_dec : ∀ n m : Nbar, {n = m} + {n ≠ m}.
proof: Proof. intros n m. destruct n as [n| ]. destruct m as [m| ]. destruct (Nat.eq_dec n m) as [Hlt| Hge]. left; subst; reflexivity. right; intros H; apply Hge. inversion H; subst; reflexivity. right; intros H; discriminate H. destruct m as [m| ]. right; intros H; discriminate H. left; reflexivity. Qed.
imports: Utf8 Compare_dec NPeano Misc