proposition: Lemma OCPPerm {n : nat} : forall (cp : cartesianPower positive (S (S n))), Permutation.Permutation (CPToList cp) (CPToList (OCP cp)).
proof: Proof. intro cp. unfold OCP. unfold OCPAux. elim_eq_rect; simpl. rewrite CPLOK. apply Permuted_sort. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms