proposition: Lemma nth_split n l d : n < length l -> exists l1, exists l2, l = l1 ++ nth n l d :: l2 /\ length l1 = n.
proof: Proof. revert l. induction n as [|n IH]; intros [|a l] H; try easy. - exists nil; exists l; now simpl. - destruct (IH l) as (l1 & l2 & Hl & Hl1); [now apply Nat.succ_lt_mono|]. exists (a::l1); exists l2; simpl; split; now f_equal. Qed.
imports: PeanoNat