proposition: Lemma insert_map_seqZ start xs i x: start ≤ i < start + Z.of_nat (length xs) → <[i:=x]> (map_seqZ start xs) =@{M A} map_seqZ start (<[Z.to_nat (i - start):=x]> xs).
proof: Proof. intros. apply map_eq. intros j. destruct (decide (i = j)) as [->|?]. - rewrite lookup_insert, lookup_map_seqZ, option_guard_True by lia. by rewrite list_lookup_insert by lia. - rewrite lookup_insert_ne, !lookup_map_seqZ by done. case_guard; [|done]. by rewrite list_lookup_insert_ne by lia. Qed.
imports: Coq(Permutation) stdpp(options)