proposition: Lemma sle_last_cons x k ks : uniq (k :: ks) -> x \in k::ks -> x <=[k::ks] (last k ks).
proof: Proof. move=>/= /andP [U1 U2]. rewrite inE sle_cons; case: eqP=>//= /eqP Nxk K. by rewrite (last_notin K) //=; apply: sle_last. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)