proposition: Lemma nthCircPerm1Eq {T:Type} {n:nat} : forall (cp : cartesianPower T (S (S n))) (Default : T), nthCP 1 cp Default = nthCP (S (S n)) (consTailCP (tailCP cp) (headCP cp)) Default.
proof: Proof. intros cp Default. apply nthCircPerm1. reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality