proposition: Lemma slt_last_cons x k ks : uniq (k :: ks) -> x \in k::ks -> last k ks != x -> x <[k::ks] (last k ks).
proof: Proof. move=>U X N; rewrite slt_neqAle; last by rewrite X. by rewrite eq_sym N sle_last_cons. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)