proposition: Lemma nthCircPerm1 {T:Type} {n:nat} : forall (cp : cartesianPower T (S (S n))) (t Default : T), t = nthCP 1 cp Default -> t = nthCP (S (S n)) (consTailCP (tailCP cp) (headCP cp)) Default.
proof: Proof. intros cp t Default Hnth. apply nthFirst in Hnth. rewrite <- Hnth. clear Hnth. unfold nthCP. rewrite consTailOK. rewrite app_nth2. rewrite <- lengthOfCPToList. simpl. rewrite <- Minus.minus_diag_reverse. reflexivity. rewrite <- lengthOfCPToList. simpl. intuition. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality