proposition: Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
proof: Proof. unfold eqke, ltk; intuition; simpl in *; subst. match goal with H : lt _ _, H1 : eq _ _ |- _ => exact (lt_not_eq H H1) end. Qed.
imports: SetoidList Morphisms OrdersTac