proposition: Lemma consecP_nilp_filter ks (p : pred _) t1 t2 : uniq ks -> consec (filter p ks) t1 t2 <-> if p t2 then [/\ t1 <[ks] t2, p t1 & nilp (filter p (&=ks `]t1, t2[))] else [/\ t1 \in ks, p t1 & nilp (filter p (&=ks `]t1, +oo[))].
proof: Proof. move=>U; case: ifP=>P2; split. - case/consecP=>Cx Nx. move: (slt_memE Cx); rewrite mem_filter=>/andP [P1 K1]. rewrite slt_filter ?(P1,P2,orbT) // in Cx. split=>//; rewrite nilp_hasPn; apply: contra Nx. case/hasP=>x; rewrite mem_filter; case/andP=>Px. move/(mem_oo _ _ _ U); case=>N1 N2 Kx _; apply/hasP; exists x=>//. apply/mem_oo; first by apply: filter_uniq. by rewrite mem_filter !slt_filter ?(P1,P2,Px,orbT). - case=>N P1 Nx; apply/consecP; split. - by rewrite slt_filter ?(P1,P2,orbT). rewrite nilp_hasPn in Nx; apply: contra Nx. case/hasP=>x /(mem_oo _ _ _ (filter_uniq _ U)); rewrite mem_filter. case=>/andP [Px Kx] X1 X2 _. rewrite !slt_filter ?(P1,P2,Px,orbT) // in X1 X2. by apply/hasP; exists x=>//; rewrite mem_filter Px /=; apply/mem_oo. - case/consecP=>Cx Nx. move: (slt_memE Cx); rewrite mem_filter=>/andP [P1 K1]. split=>//; rewrite nilp_hasPn; apply: contra Nx. case/hasP=>x; rewrite mem_filter=>/andP [Px] /(mem_ou _ _ U) [Nx Kx] _. apply/hasP; exists x=>//; apply/mem_oo; first by apply: filter_uniq. rewrite mem_filter Px Nx; split=>//. - by rewrite slt_filter ?(P1,Px,orbT). by apply: slt_memI; rewrite mem_filter ?Px // P2. case=>K1 P1 Nx; apply/consecP; split. - apply: slt_memI; first by rewrite mem_filter P1 K1. by rewrite mem_filter P2. rewrite nilp_hasPn in Nx; apply: contra Nx. case/hasP=>x /(mem_oo _ _ _ (filter_uniq _ U)); rewrite mem_filter. case=>/andP [Px Kx N1 N2] _. apply/hasP; exists x=>//; rewrite mem_filter Px /=. apply/mem_ou=>//; split=>//. by rewrite slt_filter ?(P1,Px,orbT) in N1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)