proposition: Lemma nth_indep : forall l n d d', n < length l -> nth n l d = nth n l d'.
proof: Proof. intro l; induction l as [|? ? IHl]. - inversion 1. - intros [|n] d d'; [intros; reflexivity|]. intros H. apply IHl. now apply Nat.succ_lt_mono. Qed.
imports: PeanoNat