proposition: Lemma lookup_seqZ m n i m' : seqZ m n !! i = Some m' ↔ m' = m + Z.of_nat i ∧ Z.of_nat i < n.
proof: Proof. destruct (Z_le_gt_dec n (Z.of_nat i)). - rewrite lookup_seqZ_ge by lia. naive_solver lia. - rewrite lookup_seqZ_lt by lia. naive_solver lia. Qed.
imports: stdpp(options)