proposition: Theorem compare_cont_refl p c : compare_cont c p p = c.
proof: Proof. now induction p. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef