proposition: Lemma take_iota k m n : take k (iota m n) = iota m (minn k n).
proof: Proof. have [lt_k_n|le_n_k] := ltnP. by elim: k n lt_k_n m => [|k IHk] [|n] //= H m; rewrite IHk. by apply: take_oversize; rewrite size_iota. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)