proposition: Lemma drop_iota k m n : drop k (iota m n) = iota (m + k) (n - k).
proof: Proof. by elim: k m n => [|k IHk] m [|n] //=; rewrite ?addn0 // IHk addnS subSS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)