proposition: Lemma eqsl_kk1 (s : seq A) l r k : &=s (Interval (BSide l k) (BSide r k)) = if [&& l, ~~ r & k \in s] then [:: k] else [::].
proof: Proof. rewrite /eq_slice /= slice_kk onth_index. apply/esym; case: ifP; first by case/and3P=>->->->. move/negbT; rewrite !negb_and negbK. case/or3P=>[/negbTE->|->|/negbTE->] //=. - by rewrite andbF. by rewrite if_same. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)