proposition: Lemma CoappDupPerm {m : nat} : forall (cp : cartesianPower positive m), ~ List.NoDup (CPToList cp) -> exists e, exists l, Permutation.Permutation (CPToList (ListToCP (e :: e :: l) e)) (CPToList cp).
proof: Proof. intros cp HDup. apply NotNoDupDup in HDup; try apply Pos.eq_dec. destruct HDup as [e [l1 [l2 [HEq HIn]]]]. apply in_split in HIn. destruct HIn as [l3 [l4 HEq']]. assert (HPerm := Permutation.Permutation_middle l1 l2 e). rewrite <- HEq in HPerm; clear HEq. rewrite HEq' in HPerm; clear HEq'; clear l1; clear l2; rename l3 into l1; rename l4 into l2. assert (HPerm' := Permutation.Permutation_middle l1 l2 e). apply (Permutation.perm_skip e) in HPerm'. assert (HPerm'' := Permutation.perm_trans HPerm' HPerm); clear HPerm; clear HPerm'; rename HPerm'' into HPerm. rewrite <- CPLOK with (e :: e :: l1 ++ l2) e in HPerm. exists e; exists (l1 ++ l2); assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets