proposition: Lemma eqsl_filter (p : pred A) b1 t1 b2 t2 s : (t1 \notin s) || (p t1 && ((t2 \notin s) || p t2)) -> &= (filter p s) (Interval (BSide b1 t1) (BSide b2 t2)) = filter p (&= s (Interval (BSide b1 t1) (BSide b2 t2))).
proof: Proof. case/orP=>[N1|/andP [H1]]. - by rewrite !eqsl_notinL //= mem_filter negb_and N1 orbT. case/orP=>H2. - rewrite !eqsl_notinR //=. - by rewrite eqsl_filterR // H1 orbT. by rewrite mem_filter negb_and H2 orbT. elim: s=>//= h s IH. case/boolP: (p h)=>/= Hp; last first. - rewrite {}IH eqsl_consE; case: eqVneq=>[E1|_]. - by rewrite -E1 H1 in Hp. case: eqVneq=>[E2|_] //. by rewrite -E2 H2 in Hp. rewrite !eqsl_consE; case: eqVneq=>/=_; case: eqVneq=>//=_. - by case: ifP=>//= _; rewrite Hp. rewrite eqsl_filterL; last by rewrite H2 orbT. by case: ifP=>//= _; rewrite Hp. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)