proposition: Lemma compare_antisym p q : (q ?= p) = CompOpp (p ?= q).
proof: Proof. unfold compare. now rewrite compare_cont_antisym. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef