proposition: Lemma elem_of_seqZ m n k : k ∈ seqZ m n ↔ m ≤ k < m + n.
proof: Proof. rewrite elem_of_list_lookup. setoid_rewrite lookup_seqZ. split; [naive_solver lia|]. exists (Z.to_nat (k - m)). rewrite Z2Nat.id by lia. lia. Qed.
imports: stdpp(options)