proposition: Lemma nthLast {T:Type} {n:nat} : forall (cp : cartesianPower T (S n)) (Default : T), lastCP cp = nthCP (S n) cp Default.
proof: Proof. unfold nthCP; induction n; intros cp Default. simpl; reflexivity. rewrite lastTailOK. assert (H := IHn (tailCP cp) Default); rewrite H; clear H; clear IHn. simpl. rewrite minus_n_0. reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality