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