proposition: Lemma compare_cont_spec p q c : compare_cont c p q = switch_Eq c (p ?= q).
proof: Proof. unfold compare. revert q c. induction p as [p IHp|p IHp|]; intro q; destruct q as [q|q|]; simpl; trivial. - intros c. rewrite 2 IHp. now destruct (compare_cont Eq p q). - intros c. rewrite 2 IHp. now destruct (compare_cont Eq p q). Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef