proposition: Lemma compare_succ_l p q : switch_Eq Lt (succ p ?= q) = switch_Eq Gt (p ?= q).
proof: Proof. rewrite 2 (compare_antisym q). generalize (compare_succ_r q p). now do 2 destruct compare. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef