proposition: Lemma list_lookup_inserts_Some l i k j y : list_inserts i k l !! j = Some y ↔ (j < i ∨ i + length k ≤ j) ∧ l !! j = Some y ∨ i ≤ j < i + length k ∧ j < length l ∧ k !! (j - i) = Some y.
proof: Proof. destruct (decide (j < i)). { rewrite list_lookup_inserts_lt by done; intuition lia. } destruct (decide (i + length k ≤ j)). { rewrite list_lookup_inserts_ge by done; intuition lia. } split. - intros Hy. assert (j < length l). { rewrite <-(inserts_length l i k); eauto using lookup_lt_Some. } rewrite list_lookup_inserts in Hy by lia. intuition lia. - intuition. by rewrite list_lookup_inserts by lia. Qed.
imports: stdpp(options)