proposition: Lemma list_inserts_app_r l1 l2 l3 i : list_inserts (length l2 + i) l1 (l2 ++ l3) = l2 ++ list_inserts i l1 l3.
proof: Proof. revert i; induction l1 as [|x l1 IH]; [done|]. intros i. simpl. by rewrite plus_n_Sm, IH, insert_app_r. Qed.
imports: stdpp(options)