proposition: Lemma compare_xO_xI p q : (p~0 ?= q~1) = switch_Eq Lt (p ?= q).
proof: Proof. exact (compare_cont_spec p q Lt). Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef