proposition: Lemma take_nseq i j x : i <= j -> take i (nseq j x) = nseq i x.
proof: Proof. by move=>/subnKC <-; rewrite nseqD take_size_cat // size_nseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)