proposition: Lemma CPToListTl2 {T : Type} {n : nat} : forall (cp : cartesianPower T (S (S n))), tl (CPToList cp) = CPToList (tailCP cp).
proof: Proof. intro cp. induction n. simpl; reflexivity. apply listInd with (S n) (fst cp). apply eq_add_S. assert (H := lengthOfCPToList cp); rewrite H. simpl; reflexivity. assert (H := lengthOfCPToList (tailCP cp)); rewrite H. reflexivity. simpl; reflexivity. simpl; reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality