proposition: Lemma list_lookup_inserts l i k j : i ≤ j < i + length k → j < length l → list_inserts i k l !! j = k !! (j - i).
proof: Proof. revert i j. induction k as [|y k IH]; csimpl; intros i j ??; [lia|]. destruct (decide (i = j)) as [->|]. { by rewrite list_lookup_insert, Nat.sub_diag by (rewrite inserts_length; lia). } rewrite list_lookup_insert_ne, IH by lia. by replace (j - i) with (S (j - S i)) by lia. Qed.
imports: stdpp(options)