proposition: Lemma eqsl_filterL (p : pred A) b (y : A) s : (y \notin s) || p y -> &= (filter p s) (Interval -oo (BSide b y)) = filter p (&= s (Interval -oo (BSide b y))).
proof: Proof. case/orP=>Hy. - rewrite !eqsl_notinR //=; first by rewrite !eqsl_uu. by apply: contra Hy; rewrite mem_filter; case/andP. elim: s=>//= h s IH. case/boolP: (p h)=>/= Hp; last first. - rewrite {}IH eqsl_uL_consE; case: eqVneq=>[E|_] /=. - by rewrite -E Hy in Hp. by rewrite (negbTE Hp). rewrite !eqsl_uL_consE; case: eqVneq=>_ /=. - by case: {IH}b=>//=; rewrite Hp. by rewrite Hp IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)