proposition: Lemma mem_index_iota m n i : i \in index_iota m n = (m <= i < n).
proof: Proof. rewrite mem_iota; case le_m_i: (m <= i) => //=. by rewrite -leq_subLR subSn // -subn_gt0 -subnDA subnKC // subn_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)