proposition: Theorem compare_cont_Eq p q c : compare_cont c p q = Eq -> c = Eq.
proof: Proof. rewrite compare_cont_spec. now destruct (p ?= q). Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef