proposition: Lemma lookup_seq j n i j' : seq j n !! i = Some j' ↔ j' = j + i ∧ i < n.
proof: Proof. destruct (le_lt_dec n i). - rewrite lookup_seq_ge by done. naive_solver lia. - rewrite lookup_seq_lt by done. naive_solver lia. Qed.
imports: stdpp(options)