proposition: Lemma Peqb_true_eq x y : Pos.eqb x y = true -> x=y.
proof: Proof. apply Pos.eqb_eq. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef