proposition: Lemma findall_cat p s1 s2 : findall p (s1 ++ s2) = findall p s1 ++ map (fun n => size s1 + n) (findall p s2).
proof: Proof. rewrite !findallE size_cat iotaD add0n zip_cat; last by rewrite size_iota. rewrite filter_cat {1}/unzip1 map_cat; congr (_ ++ _). set n := size s1. rewrite -{1}(addn0 n) iotaDl zip_mapl filter_map -!map_comp. rewrite (eq_filter (a2:=(p \o snd))); last by case. by apply: eq_map; case. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)