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