proposition: Lemma list_inserts_0_r l1 l2 l3 : length l1 = length l2 → list_inserts 0 l1 (l2 ++ l3) = l1 ++ l3.
proof: Proof. revert l2. induction l1 as [|x l1 IH]; intros [|y l2] ?; simplify_eq/=; [done|]. rewrite list_inserts_cons. simpl. by rewrite IH. Qed.
imports: stdpp(options)