proposition: Theorem List_In_nth : ∀ α a la (d : α), a ∈ la → ∃ n, a = List.nth n la d.
proof: Proof. intros u a la d Ha. revert a Ha. induction la as [| b]; intros; [ contradiction | idtac ]. simpl in Ha. destruct Ha as [Ha| Ha]. subst b. exists O; reflexivity. apply IHla in Ha. destruct Ha as (n, Ha). exists (S n); simpl. assumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz