proposition: Lemma size_index_iotaz m n : size (index_iotaz m n) = if m <= n then `|n - m|%N else 0%N.
proof: Proof. case: m => m; case: n => n; rewrite /index_iotaz => //=. - rewrite size_map /index_iota size_iota. case: (leqP n m) => hnm. + rewrite lez_nat leq_eqVlt ltnNge hnm orbF; case: ifP. by move/eqP->; rewrite subnn subrr. by move=> mn; apply/eqP; rewrite subn_eq0. + by rewrite lez_nat ltnW // subzn ?(ltnW hnm) // absz_nat. - by rewrite size_cat size_rev /index_iota /= !size_map !size_iota addnC subn0. - rewrite size_map size_rev /index_iota size_iota !NegzE lerN2 lez_nat. rewrite opprK addrC; case: ifP => hnm; first by rewrite subzn. case: (altP (n =P m)) => [-> | enm]; first by rewrite subnn. apply/eqP; rewrite subn_eq0 ltnNge; move: hnm; rewrite ltnS leq_eqVlt. by rewrite (negPf enm) /= => ->. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp