proposition: Lemma compare_cont_Lt_not_Gt p q : compare_cont Lt p q <> Gt <-> p <= q.
proof: Proof. apply not_iff_compat, compare_cont_Lt_Gt. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef