proposition: Lemma map_seqZ_insert start xs i x: (i < length xs)%nat → map_seqZ start (<[i:=x]> xs) =@{M A} <[start + Z.of_nat i:=x]> (map_seqZ start xs).
proof: Proof. intros. rewrite insert_map_seqZ by lia. auto with lia f_equal. Qed.
imports: Coq(Permutation) stdpp(options)