proposition: Lemma CoappDupAux {m : nat} : forall (cp : cartesianPower positive (S (S (S m)))), ~ List.NoDup (CPToList cp) -> exists e, exists (l : list positive), exists m', exists (cp' : cartesianPower positive (S (S (S m')))), Permutation.Permutation (CPToList cp') (CPToList cp) /\ headCP cp' = e /\ headCP (tailCP cp') = e.
proof: Proof. intros cp H. apply CoappDupPerm in H. destruct H as [e[l HPerm]]. assert (Hl := Permutation.Permutation_length HPerm). rewrite CPLOK in Hl. rewrite <- lengthOfCPToList in Hl. induction l; try (simpl in Hl; discriminate); clear IHl. exists e; exists (a :: l); exists (length l); exists (ListToCP (e :: e :: a :: l) e). split; try assumption. simpl. split; reflexivity. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets