proposition: Lemma In_nth l x d : In x l -> exists n, n < length l /\ nth n l d = x.
proof: Proof. induction l as [|a l IH]. - easy. - intros [H|H]. * subst; exists 0; simpl; auto using Nat.lt_0_succ. * destruct (IH H) as (n & Hn & Hn'). apply Nat.succ_lt_mono in Hn. now exists (S n). Qed.
imports: PeanoNat