proposition: Lemma index_iotaz_add n m p : m <= n -> n <= p -> (index_iotaz m n ++ index_iotaz n p) = index_iotaz m p.
proof: Proof. move=> hmn hnp. have h : `|n - m| + `|p - n| = `|p - m|%N. move/leqifP: (leqifD_distz p n m). rewrite hnp hmn orbT addnC; move/eqP; move/(f_equal Posz). by rewrite PoszD; move<-. apply: (@eq_from_nth _ 0); rewrite size_cat !size_index_iotaz hmn hnp. - rewrite (le_trans hmn hnp); move: h; rewrite -PoszD /=; move/eqP. by rewrite eqz_nat; move/eqP. - move=> i; move: (h); rewrite -PoszD; move/eqP; rewrite eqz_nat. move/eqP-> => hi1. rewrite (nth_cat 0) size_index_iotaz. rewrite hmn; case: ifP => hi2. + by rewrite !nth_index_iotaz //;apply: le_trans hnp. have hmn' : `|n - m | = n - m by apply: ger0_norm; rewrite subr_gte0. rewrite nth_index_iotaz //; last first. rewrite -subzn; last by rewrite leqNgt hi2. by rewrite lterBDr addrC h ltz_nat. rewrite nth_index_iotaz //; last exact: le_trans hnp. rewrite -subzn; last by rewrite leqNgt hi2. move: hmn'; rewrite abszE; move->. rewrite addrCA opprB. by rewrite [_ + (_ - _)]addrCA subrr addr0 addrC. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp