proposition: Lemma takel_cat s1 s2 : n0 <= size s1 -> take n0 (s1 ++ s2) = take n0 s1.
proof: Proof. by rewrite take_cat; case: ltngtP => // ->; rewrite subnn take0 take_size cats0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)