proposition: Lemma size_take s : size (take n0 s) = if n0 < size s then n0 else size s.
proof: Proof. have [le_sn | lt_ns] := leqP (size s) n0; first by rewrite take_oversize. by rewrite size_takel // ltnW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)