proposition: Lemma eqsl_filterR (p : pred A) b (x : A) s : (x \notin s) || p x -> &= (filter p s) (Interval (BSide b x) +oo) = filter p (&= s (Interval (BSide b x) +oo)).
proof: Proof. case/orP=>Hx. - by rewrite !eqsl_notinL //= mem_filter negb_and Hx orbT. elim: s=>//=h s IH. case/boolP: (p h)=>/= Hp; last first. - rewrite {}IH eqsl_uR_consE; case: eqVneq=>[E|_] //=. by rewrite -E Hx in Hp. rewrite !eqsl_uR_consE; case: eqVneq=>//= _. by case: {IH}b=>//=; rewrite Hp. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)