proposition: Lemma lookup_map_seqZ_is_Some start xs i : is_Some (map_seqZ (M:=M A) start xs !! i) ↔ start ≤ i < start + Z.of_nat (length xs).
proof: Proof. rewrite <-not_eq_None_Some, lookup_map_seqZ_None. lia. Qed.
imports: Coq(Permutation) stdpp(options)