proposition: Lemma eqsliceLO_notin (s : seq A) x b : uniq s -> x \notin &=s (Interval (BRight x) b).
proof: Proof. rewrite /eq_slice /slice /= addn1 => U. move: (mem_drop_indexlast x s); rewrite indexlast_uniq //. by apply/contra/prefix_drop_sub/prefix_take. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)