proposition: Lemma consecP_filter ks (p : pred _) t1 t2 : uniq ks -> consec (filter p ks) t1 t2 <-> if p t2 then [/\ t1 <[ks] t2, p t1 & {in &=ks `]t1, t2[ , forall z, ~~ p z}] else [/\ t1 \in ks , p t1 & {in &=ks `]t1, +oo[, forall z, ~~ p z}].
proof: Proof. move=>U; split=>[|H]. - by move/(consecP_nilp_filter _ _ _ U); case: ifP=>P [?? /nilp_filter]. by apply/consecP_nilp_filter; case: ifP H=>P [?? /nilp_filter]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)