proposition: Lemma nth_error_app2 l l' n : length l <= n -> nth_error (l++l') n = nth_error l' (n-length l).
proof: Proof. revert l. induction n as [|n IHn]; intros [|a l] H; [easy ..|]. cbn. now apply IHn, Nat.succ_le_mono. Qed.
imports: PeanoNat