proposition: Lemma map_seq_insert start xs i x: i < length xs → map_seq start (<[i:=x]> xs) =@{M A} <[start + i:=x]> (map_seq start xs).
proof: Proof. intros. rewrite insert_map_seq by lia. auto with f_equal lia. Qed.
imports: Coq(Permutation) stdpp(options)