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