proposition: Lemma InNth {T:Type} {n:nat} : forall (cp : cartesianPower T n) (t Default : T), InCP t cp -> (exists id, id >= 1 /\ id <= n /\ t = nthCP id cp Default).
proof: Proof. induction n; intros cp t Default HIn. unfold InCP in HIn. simpl in HIn. intuition. induction n. exists 1; try intuition. unfold nthCP; simpl. unfold InCP in HIn; simpl in HIn. intuition. clear IHn0. apply InCPOK in HIn. elim HIn; clear HIn; intro HIn. exists 1; unfold nthCP; simpl; intuition. assert (H := IHn (tailCP cp) t Default). apply H in HIn; clear H. destruct HIn as [id [Hge [Hle HEq]]]. unfold nthCP in *. exists (S id); try intuition. assert (H := app_nth2 ((headCP cp) :: nil) (CPToList (tailCP cp)) Default Hge). rewrite CPToListOK. assert (H' : (headCP cp :: nil) ++ CPToList (tailCP cp) = (headCP cp :: CPToList (tailCP cp))) by (simpl; reflexivity); rewrite <- H'; clear H'. assert (H' : (S id - 1) = id) by (simpl; rewrite minus_n_0; reflexivity); rewrite H'; clear H'. rewrite H. apply HEq. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality