proposition: Lemma nthCPTlOK {T:Type} {m:nat} : forall (cp : cartesianPower T (S (S m))) (Default : T) n, nthCP (S n) (tailCP cp) Default = nthCP (S (S n)) cp Default.
proof: Proof. induction m; intros cp Default n. induction n; unfold nthCP; simpl; reflexivity. assert (H := nthCircPerm2 cp (nthCP (S (S n)) cp Default) Default n). assert (Hnm := le_lt_dec n (S m)). elim Hnm; clear Hnm; intro Hnm. assert (H' : nthCP (S (S n)) cp Default = nthCP (S (S n)) cp Default) by reflexivity; apply H in H'; try assumption; clear H; rewrite H'; clear H'. unfold nthCP. rewrite consTailOK. rewrite app_nth1; try reflexivity. rewrite <- lengthOfCPToList. simpl. rewrite minus_n_0. apply Lt.le_lt_n_Sm; assumption. unfold nthCP. rewrite nth_overflow. rewrite nth_overflow; try reflexivity. rewrite <- lengthOfCPToList; simpl; intuition. rewrite <- lengthOfCPToList; simpl; rewrite minus_n_0; intuition. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality