proposition: Lemma nth_error_length : forall (ls ls' : list T) n, nth_error (ls ++ ls') (n + length ls) = nth_error ls' n.
proof: Proof. induction ls; simpl; intros. rewrite Nat.add_0_r. auto. rewrite <-Nat.add_succ_comm. simpl. eapply IHls. Qed.
imports: Coq.Lists.List Coq.Arith.PeanoNat