proposition: Lemma eqslice_split (s : seq A) (i : interval A) b (x : A) : ix_bnd s i.1 <= BSide b (index x s) <= ix_bnd s i.2 -> &=s i = &=s (Interval i.1 (BSide b x)) ++ &=s (Interval (BSide b x) i.2).
proof: Proof. by case: i=>i j H; rewrite /eq_slice; apply: slice_split_bnd. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)