proposition: Lemma nthCP01 {T:Type} {n:nat} : forall (cp : cartesianPower T (S n)) Default, nthCP 0 cp Default = nthCP 1 cp Default.
proof: Proof. unfold nthCP. assert (H : 0 - 1 = 0) by (simpl; reflexivity); rewrite H; clear H. assert (H : 1 - 1 = 0) by (simpl; reflexivity); rewrite H; clear H. reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality