proposition: Lemma list_inserts_app_l l1 l2 l3 i : list_inserts i (l1 ++ l2) l3 = list_inserts (length l1 + i) l2 (list_inserts i l1 l3).
proof: Proof. revert i; induction l1 as [|x l1 IH]; [done|]. intro i. simpl. rewrite IH, Nat.add_succ_r. apply list_insert_inserts_lt. lia. Qed.
imports: stdpp(options)