proposition: Lemma size_takel s : n0 <= size s -> size (take n0 s) = n0.
proof: Proof. by move/subKn; rewrite -size_drop -[in size s](cat_take_drop s) size_cat addnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)