proposition: Lemma lookup_map_seqZ_Some_inv start xs i x : xs !! i = Some x ↔ map_seqZ (M:=M A) start xs !! (start + Z.of_nat i) = Some x.
proof: Proof. rewrite ->lookup_map_seqZ, option_guard_True by lia. assert (Z.to_nat (start + Z.of_nat i - start) = i) as -> by lia. done. Qed.
imports: Coq(Permutation) stdpp(options)