proposition: Lemma list_insert_inserts_lt l i j x k : i < j → <[i:=x]>(list_inserts j k l) = list_inserts j k (<[i:=x]>l).
proof: Proof. revert i j. induction k; intros i j ?; simpl; rewrite 1?list_insert_commute by lia; auto with f_equal. Qed.
imports: stdpp(options)