proposition: Lemma list_decompose k {X} (A: list X): k <= length A -> exists A1 A2, A = A1 ++ A2 /\ length A1 = k.
proof: Proof. induction A in k |-*; intros. - exists nil. exists nil; cbn. destruct k; intuition easy. - destruct k. + exists nil; exists (a :: A); intuition easy. + cbn in *; assert (k <= length A) by lia. destruct (IHA _ H0) as (A1 & A2 & ?). intuition idtac. exists (a :: A1). exists A2. subst. intuition easy. Qed.
imports: List Lia