proposition: Lemma nth_inspos s pos i n : pos <= size s -> nth Z ((take pos s) ++ n :: (drop pos s)) i = if i == pos then n else nth Z s (shiftinv_pos pos i).
proof: Proof. Proof using. move=> Hpos. case: (i =P pos) => [->{i} | /eqP Hipos]. by rewrite nth_cat size_takel // ltnn subnn. rewrite /shiftinv_pos nth_cat size_take. case (ltnP pos (size s)) => [{}Hpos | Hpos2]. - case: (ltnP i pos) => Hi; first by rewrite (nth_take _ Hi). have {Hipos}Hi : pos < i by rewrite ltn_neqAle eq_sym Hipos Hi. case: i Hi => //= i; rewrite ltnS => Hi. by rewrite (subSn Hi) /= nth_drop (subnKC Hi). - have {Hpos2}Hpos : pos = size s by apply anti_leq; rewrite Hpos Hpos2. subst pos. case: (ltnP i (size s)) => Hisz; first by rewrite (nth_take _ Hisz). have {Hipos Hisz} : size s < i by rewrite ltn_neqAle eq_sym Hisz Hipos. case: i => //= i; rewrite ltnS => Hi. by rewrite (subSn Hi) /= nth_drop (subnKC Hi). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools