proposition: Lemma nth_overflow : forall l n d, length l <= n -> nth n l d = d.
proof: Proof. intro l; induction l as [|? ? IHl]; intro n; destruct n; simpl; intros d H; auto. - inversion H. - apply IHl. now apply Nat.succ_le_mono. Qed.
imports: PeanoNat