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