proposition: Lemma circPermNIdFirst {T:Type} {n:nat} : forall (cp : cartesianPower T (S (S n))) (Default : T), nthCP 1 cp Default = nthCP 1 (circPermNCP (S (S n)) cp) Default.
proof: Proof. intros cp Default. rewrite nthCircPerm1Eq. assert (H : 0 + S n <= S n) by intuition. assert (H' := nthCircPermNAny (consTailCP (tailCP cp) (headCP cp)) Default 0 (S n) H); clear H. assert (H : 1 + S n = S (S n)) by intuition; rewrite H in H'; clear H; rewrite H'. apply eq_sym. rewrite circPermNCPOK. reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality