proposition: Lemma eqsliceRO_notin s x a : x \notin &=s (Interval a (BLeft x)).
proof: Proof. rewrite /eq_slice /slice /= addn0. apply/negP=>/mem_drop; apply/negP. by apply: mem_take_index. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)