proposition: Lemma drop_nseq i j x : drop i (nseq j x) = nseq (j - i) x.
proof: Proof. case: (leqP i j) => [/subnKC {1}<-|/ltnW j_le_i]. by rewrite nseqD drop_size_cat // size_nseq. by rewrite drop_oversize ?size_nseq // (eqP j_le_i). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)