proposition: Lemma list_lookup_inserts_ge l i k j : i + length k ≤ j → list_inserts i k l !! j = l !! j.
proof: Proof. revert i j. induction k; csimpl; intros i j ?; rewrite ?list_lookup_insert_ne by lia; auto with lia. Qed.
imports: stdpp(options)