proposition: Lemma drop_drop s n1 n2 : drop n1 (drop n2 s) = drop (n1 + n2) s.
proof: Proof. by elim: s n2 => // x s ihs [|n2]; rewrite ?drop0 ?addn0 ?addnS /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)