proposition: Corollary olt_ole_last' k s x t : uniq (k::s) -> t != k -> x <[k::s] t = x <=[k::s] (last k (&=(k::s) `]-oo, t[)).
proof: Proof. by move=>U K; rewrite olt_ole_last // eqsl_uL_consE (negbTE K). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)