proposition: Lemma OCPALengthOK {n : nat} : forall (cp : cartesianPower positive (S (S n))), (length (OCPAux cp)) = (S (S n)).
proof: Proof. intro cp. unfold OCPAux. assert (HPerm := Permuted_sort (CPToList cp)). apply Permutation.Permutation_length in HPerm. rewrite <- HPerm. apply eq_sym. apply lengthOfCPToList. Defined.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms