proposition: Lemma eqsl_ou_split t (s1 s2 : seq A) : t \notin s1 -> &=(s1++t::s2) `]t, +oo[ = s2.
proof: Proof. by move=>X1; rewrite eqsl_uR_catE (negbTE X1) eqsl_uR_consE eqxx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)