proposition: Lemma mem_prefixesP w p : reflect (exists i, p = take i w) (p \in prefixes w).
proof: Proof. rewrite /prefixes; apply (iffP idP) => [/mapP[i _ ->] | [i ->]]. - by exists i. - exact: take_prefixes. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree