proposition: Theorem eqb_eq p q : (p =? q) = true <-> p=q.
proof: Proof. revert q. induction p as [p IHp|p IHp|]; intro q; destruct q; simpl; rewrite ?IHp; split; congruence. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef