proposition: Corollary eqsl_xxou (ks : seq A) t1 t2 : t1 <=[ks] t2 -> &=ks `[t1, +oo[ = &=ks `[t1, t2] ++ &=ks `]t2, +oo[.
proof: Proof. by move=>H; apply: eqslice_split=>/=; rewrite andbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)