proposition: Lemma gtb_1 : forall p p', gtb p p' = true <-> ltk p' p.
proof: Proof. intros (x,e) (y,e'); unfold gtb, O.ltk; simpl. destruct (E.compare x y); intuition; try discriminate; ME.order. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface