proposition: Lemma compare_cont_antisym p q c : CompOpp (compare_cont c p q) = compare_cont (CompOpp c) q p.
proof: Proof. revert q c. induction p as [p IHp|p IHp| ]; intros [q|q| ] c; simpl; trivial; apply IHp. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef