proposition: Lemma lookup_map_seqZ_None start xs i : map_seqZ (M:=M A) start xs !! i = None ↔ i < start ∨ start + Z.of_nat (length xs) ≤ i.
proof: Proof. rewrite lookup_map_seqZ. case_guard; simplify_option_eq; rewrite ?lookup_ge_None; naive_solver lia. Qed.
imports: Coq(Permutation) stdpp(options)