proposition: Lemma compare_cont_Lt_Lt p q : compare_cont Lt p q = Lt <-> p <= q.
proof: Proof. rewrite compare_cont_spec. unfold le. destruct (p ?= q); easy'. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef