proposition: Lemma mem_index_iota : forall m n i, i \in index_iota m n = (m <= i < n).
proof: Proof. move=> m n i; rewrite mem_iota; case le_m_i: (m <= i) => //=. by rewrite -leq_sub_add leq_subS // -subn_gt0 subn_sub addnC subnK // subn_gt0. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops