proposition: Lemma split_nth : forall (l:list (A*B))(n:nat)(d:A*B), nth n l d = (nth n (fst (split l)) (fst d), nth n (snd (split l)) (snd d)).
proof: Proof. intro l; induction l as [|a l IHl]. - intros n d; destruct n; destruct d; simpl; auto. - intros n d; destruct n; destruct d; simpl; auto. + destruct a; destruct (split l); simpl; auto. + destruct a; destruct (split l); simpl in *; auto. Qed.
imports: PeanoNat