proposition: Lemma nth_error_app_L : forall (A B : list T) n, n < length A -> nth_error (A ++ B) n = nth_error A n.
proof: Proof. induction A; destruct n; simpl; intros; auto. { inversion H. } { inversion H. } { eapply IHA. apply Nat.succ_lt_mono; assumption. } Qed.
imports: Coq.Lists.List Coq.Arith.PeanoNat