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