proposition: Fact list_pick X (ll : list X) k : k < length ll -> { x : _ & { l : _ & { r | ll = l++x::r /\ length l = k } } }.
proof: Proof. revert k; induction ll as [ | x ll IHll ]; intros k. simpl; lia. destruct k as [ | k ]; intros H. exists x, nil, ll; simpl; auto. simpl in H. destruct IHll with (k := k) as (y & l & r & ? & ?); try lia. exists y, (x::l), r; subst; simpl; split; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)