proposition: Lemma drop_cat s1 s2 : drop n0 (s1 ++ s2) = if n0 < size s1 then drop n0 s1 ++ s2 else drop (n0 - size s1) s2.
proof: Proof. by elim: s1 n0 => [|x s1 IHs] []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)