proposition: Lemma eq_dec (x y: positive): {x = y} + {x <> y}.
proof: Proof. intros. case_eq (x ?= y); intros. - left. now apply Pos.compare_eq. - right. intro. subst y. now rewrite (Pos.compare_refl x) in *. - right. intro. subst y. now rewrite (Pos.compare_refl x) in *. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec