proposition: Lemma findall_auxE oi0 p s : (forall s1 s2 : seq nat, oi0.1 (s1 ++ s2) = oi0.1 s1 ++ s2) -> let: (rs, ix) := findall_aux oi0 p s in (forall s' : seq nat, rs s' = oi0.1 (unzip1 (filter (p \o snd) (zip (iota oi0.2 (size s)) s))) ++ s') /\ ix = oi0.2 + size s.
proof: Proof. move; rewrite /findall_aux; elim: s oi0=>[|x s IH] [o0 i0] /= H0. - split; last by rewrite addn0. by move=>s'; rewrite -{1}(cat0s s') H0. case/boolP: (p x)=>/= Hpx. - move: (IH (o0 \o cons i0, i0.+1))=>/=. rewrite addSn addnS; apply=>s1 s2. by rewrite -cat_cons H0. by move: (IH (o0, i0.+1))=>/=; rewrite addSn addnS; apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)