proposition: Lemma nthCircPerm2 {T:Type} {n:nat} : forall (cp : cartesianPower T (S (S n))) (t Default : T) id, t = nthCP (S (S id)) cp Default -> id <= n -> t = nthCP (S id) (consTailCP (tailCP cp) (headCP cp)) Default.
proof: Proof. induction n; intros cp t Default id Hnth HIn. simpl in *. induction id. unfold nthCP in *. simpl in Hnth. rewrite <- Hnth. simpl; reflexivity. assert (H := Le.le_Sn_0 id); intuition. unfold nthCP in *. rewrite consTailOK. rewrite CPLHdTlOK in Hnth. rewrite app_nth2 in Hnth. assert (H : S (S id) - 1 - length (headCP cp :: nil) = S id - 1) by (simpl; reflexivity); rewrite H in Hnth; clear H. rewrite app_nth1; try assumption. rewrite <- lengthOfCPToList. simpl. rewrite minus_n_0. apply Lt.le_lt_n_Sm; assumption. simpl. intuition. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality