proposition: Lemma app_nth2 : forall l l' d n, n >= length l -> nth n (l++l') d = nth (n-length l) l' d.
proof: Proof. intro l; induction l as [|? ? IHl]; intros l' d [|n]; auto. - inversion 1. - intros; simpl; rewrite IHl; [reflexivity|now apply Nat.succ_le_mono]. Qed.
imports: PeanoNat