proposition: Lemma gtb_1 : forall p p', gtb p p' = true <-> ltk p' p.
proof: Proof. intros (x,e) (y,e'); unfold gtb; klean. case K.compare_spec; intuition; try discriminate; F.order. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)