proposition: Lemma olt_ole_last k s x t : uniq (k::s) -> t != k -> x <[k::s] t = x <=[k::s] (last k (&=s `]-oo, t[)).
proof: Proof. elim: s k=>/= [|y s IH] k //=. - rewrite slt_cons slt_nil sle_cons sle_nil andbT eqxx orbF. by move=>_ ->. rewrite inE negb_or -andbA; case/and4P=>Nky K Y U Nkt. rewrite slt_cons sle_cons Nkt /=; case: (eqVneq x k)=>//= Nkx. rewrite eqsl_uL_consE; case: (eqVneq t y)=>/= [E|Nty]. - by rewrite eqxx /= E sltR. suff -> /= : last y (&=s `]-oo, t[) != k by rewrite IH //= Y. apply: contraTneq (mem_last y (&=s `]-oo, t[))=> E. rewrite inE E negb_or Nky /=; apply: contra K. by exact: slice_subset_full. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)