proposition: Lemma CPLOCPTlOK {n : nat} : forall (cp : cartesianPower positive (S (S (S n)))), headCP cp = headCP (OCP cp) -> CPToList (OCP (tailCP cp)) = CPToList (tailCP (OCP cp)).
proof: Proof. intros cp Hhd. apply PermSorted. assert (H := OCPPerm cp). rewrite CPToListOK in H. apply Permutation.Permutation_sym in H. rewrite CPToListOK in H. rewrite <- Hhd in H. apply Permutation.Permutation_app_inv_l with ((headCP cp) :: nil). assert (H' : (headCP cp :: nil) ++ CPToList (OCP (tailCP cp)) = headCP cp :: (CPToList (OCP (tailCP cp)))) by (simpl; reflexivity); rewrite H'; clear H'. assert (H' : (headCP cp :: nil) ++ CPToList (tailCP (OCP cp)) = headCP cp :: (CPToList (tailCP (OCP cp)))) by (simpl; reflexivity); rewrite H'; clear H'. apply Permutation.Permutation_sym in H. apply Permutation.perm_trans with (headCP cp :: CPToList (tailCP cp)); try assumption; clear H. assert (H := OCPPerm (tailCP cp)). apply Permutation.Permutation_sym in H. apply Permutation.perm_skip. assumption. apply OCPSortedAux. rewrite <- CPToListTl2. apply OCPSortedTl. apply OCPSortedAux. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms