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