proposition: Lemma circPermNIdAux {T:Type} {n:nat} : forall (cp : cartesianPower T (S (S n))) (Default : T), cp = circPermNCP (S (S n)) cp.
proof: Proof. intros cp Default. apply nthEqOK with Default. intro m. assert (Hmn := le_lt_dec m (S (S n))). elim Hmn; clear Hmn; intro Hmn. revert cp; induction m; intro cp. do 2 (rewrite nthCP01). apply circPermNIdFirst. clear IHm. revert cp; induction m; intro cp. apply circPermNIdFirst. assert (H : m <= n) by (do 2 (apply le_S_n); assumption). rewrite nthCircPerm2Eq; try assumption; clear H. assert (H : S m <= S (S n)) by intuition. rewrite IHm; try assumption; clear H; clear IHm. rewrite <- circPermNCPOK. rewrite circPermPerm. assert (H : m + 1 <= S n) by (rewrite plus_n_1; intuition). rewrite <- nthCircPermNAny; try assumption; clear H. rewrite plus_n_1; reflexivity. induction m. assert (H := lt_n_0 (S (S n))); intuition. clear IHm. unfold nthCP. rewrite nth_overflow. rewrite nth_overflow; try reflexivity. rewrite <- lengthOfCPToList. simpl. rewrite minus_n_0. apply gt_S_le. assumption. rewrite <- lengthOfCPToList. simpl. rewrite minus_n_0. apply gt_S_le. assumption. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality