proposition: Lemma nth_index_iotaz m n i : m <= n -> (Posz i < `|n - m|) -> (index_iotaz m n)`_i = m + (Posz i).
proof: Proof. case: m => m; case: n => n // hmn hi; rewrite /index_iotaz /=. - rewrite (nth_map 0%N) /index_iota; last first. by rewrite size_iota //; move: hi; rewrite subzn. rewrite -natz nth_iota; first by rewrite natrD !natz. suff <- : `|n - m|%N = (n - m)%N by []. by rewrite subzn //; apply/normr_idP; rewrite natz PoszD. - rewrite nth_cat size_rev /= size_map size_iota. case: ifP => him. - rewrite nth_rev /= size_map ?size_iota // subSS !NegzE. have -> : - Posz (m.+1) + Posz i = - Posz (m - i) -1. by rewrite -addn1 PoszD -subzn // opprD opprB addrAC [-Posz m + i]addrC. case ek : (m - i)%N => [ | k] //=. rewrite (nth_map 0%N). rewrite nth_iota; last by rewrite -ek leq_subr. by rewrite NegzE -addnS PoszD opprD addrC. by rewrite size_iota -ek leq_subr. - have {}hi : (i - m.+1 < n)%N. move: hi; rewrite NegzE opprK -PoszD ger0_norm //. by rewrite PoszD -lterBDr subzn ?ltz_nat // ltnNge -ltnS him. rewrite (nth_map 0%N); last by rewrite /index_iota size_iota subn0. rewrite /index_iota subn0 nth_iota // add0n NegzE addrC subzn //. by rewrite ltnNge -ltnS him. - have {}hmn : (n <= m)%N. by move: hmn; rewrite !NegzE lerNl opprK lez_nat. have hi' : (i < m - n)%N. by move: hi; rewrite !NegzE opprK addrC subzn. have hi'' : (i <= m)%N. apply: leq_trans (leq_subr n m); exact: ltnW. rewrite (nth_map 0%N); last first. by rewrite size_rev /index_iota size_iota subSS. rewrite /index_iota nth_rev !size_iota ?subSS //. rewrite nth_iota; last by rewrite subnSK // leq_subLR leq_addl. rewrite !NegzE addnBA // addSn subSS subnKC // -subSn //. by rewrite -subzn 1?ltnW // opprB addrC //. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp