proposition: Lemma eq_dec : forall x y:positive, {x = y} + {x <> y}.
proof: Proof. decide equality. Defined.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef