proposition: Lemma compare_cont_Lt_not_Lt p q : compare_cont Lt p q <> Lt <-> p > q.
proof: Proof. rewrite compare_cont_Lt_Lt. unfold gt, le, compare. now destruct compare_cont; split; try apply comparison_eq_stable. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef