proposition: Lemma mem_index_iotaz m n i : i \in index_iotaz m n = (m <= i < n).
proof: Proof. case: m => m; case: n => n; rewrite /index_iotaz. - apply/mapP/idP. by case=> xi; rewrite mem_index_iota => hi ->; rewrite ltz_nat. by case: i => // xi; rewrite ltz_nat => hi; exists xi; rewrite ?mem_index_iota. - by rewrite in_nil; case: i => xi //; rewrite andbF. - rewrite mem_cat; apply/orP/idP => [[] | ]. + rewrite mem_rev; case/mapP=> xi; rewrite mem_iota add0n; case/andP=> _ hi ->. by rewrite andbT !NegzE lerN2 /= lez_nat. + case/mapP=> xi; rewrite mem_index_iota; case/andP=> _ hi -> /=. by rewrite ltz_nat. case: i => xi. + by rewrite /= => hi; right; apply/mapP; exists xi; rewrite // mem_index_iota. + rewrite andbT {1}(NegzE xi) (NegzE m) lerN2 => hi; left; rewrite mem_rev. rewrite mem_map ?mem_index_iota //; exact: Negz_inj. - apply/idP/idP. case/mapP=> xi; rewrite mem_rev mem_index_iota => hi ->. by rewrite !NegzE lerN2 ltrN2 andbC ltz_nat lez_nat. case: i => // xi; rewrite !NegzE lerN2 ltrN2 lez_nat ltz_nat andbC => hi. rewrite -NegzE mem_map; last exact: Negz_inj. by rewrite mem_rev mem_index_iota. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp