proposition: Lemma take_cat s1 s2 : take n0 (s1 ++ s2) = if n0 < size s1 then take n0 s1 else s1 ++ take (n0 - size s1) s2.
proof: Proof. elim: s1 n0 => [|x s1 IHs] [|n] //=. by rewrite ltnS subSS -(fun_if (cons x)) -IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)