proposition: Lemma Exists_nth l : Exists l <-> exists i d, i < length l /\ P (nth i l d).
proof: Proof. split. - intros HE; apply Exists_exists in HE. destruct HE as [a [Hin HP]]. apply (In_nth _ _ a) in Hin; destruct Hin as [i [Hl Heq]]. rewrite <- Heq in HP. now exists i; exists a. - intros [i [d [Hl HP]]]. apply Exists_exists; exists (nth i l d); split. + apply nth_In; assumption. + assumption. Qed.
imports: PeanoNat