proposition: Lemma consTailCPOK {T:Type} {n:nat} : forall (cp : cartesianPower T (S (S n))), cp = consTailCP (allButLastCP cp) (lastCP cp).
proof: Proof. intro cp. induction n. simpl. apply CPPair. apply CP_ind. simpl; reflexivity. assert (H := IHn (tailCP cp)). rewrite <- lastCPTl in H. rewrite allButLastCPTl in H. rewrite <- consTailCPTl in H. assumption. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality