proposition: Lemma mem_iota m n i : (i \in iota m n) = (m <= i < m + n).
proof: Proof. elim: n m => [|n IHn] /= m; first by rewrite addn0 ltnNge andbN. by rewrite in_cons IHn addnS ltnS; case: ltngtP => // ->; rewrite leq_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)