proposition: Lemma combine_nth : forall (l:list A)(l':list B)(n:nat)(x:A)(y:B), length l = length l' -> nth n (combine l l') (x,y) = (nth n l x, nth n l' y).
proof: Proof. intro l; induction l; intro l'; destruct l'; intros n x y; try discriminate. - destruct n; simpl; auto. - destruct n; simpl in *; auto. Qed.
imports: PeanoNat