proposition: Lemma take_prefixes w i : take i w \in prefixes w.
proof: Proof. apply/mapP; case (leqP i (size w)) => Hi. - by exists i; first by rewrite mem_iota add0n ltnS Hi. - exists (size w); first by rewrite mem_iota add0n ltnS leqnn. rewrite take_size take_oversize //. exact: ltnW. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree