proposition: Lemma has_take_leq (p : pred T) (s : seq T) i : i <= size s -> has p (take i s) = (find p s < i).
proof: Proof. by elim: s i => [|y s ihs] [|i]//=; case: (p _) => //= /ihs ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)