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