proposition: Lemma take_insert_lt l n i x : i < n → take n (<[i:=x]>l) = <[i:=x]>(take n l).
proof: Proof. revert l i. induction n as [|? IHn]; auto; simpl. intros [|] [|] ?; auto; simpl. by rewrite IHn by lia. Qed.
imports: stdpp(options)