proposition: Lemma nth_error_split l n a : nth_error l n = Some a -> exists l1, exists l2, l = l1 ++ a :: l2 /\ length l1 = n.
proof: Proof. revert l. induction n as [|n IH]; intros [|x l] H; [easy| |easy|]. - exists nil; exists l. now injection H as [= ->]. - destruct (IH _ H) as (l1 & l2 & H1 & H2). exists (x::l1); exists l2; simpl; split; now f_equal. Qed.
imports: PeanoNat