proposition: Lemma compare_eq_iff p q : (p ?= q) = Eq <-> p = q.
proof: Proof. rewrite compare_sub_mask, <- sub_mask_nul_iff. destruct sub_mask; now split. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef