proposition: Lemma drop_nilE s m : (drop m s == [::]) = (size s <= m).
proof: Proof. by elim: m s => [|m IHm] [|s0 s] //=; rewrite IHm ltnS. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)