proposition: Lemma OCPSortedAux {n : nat} : forall (cp : cartesianPower positive (S (S n))), StronglySorted (fun x x0 : positive => is_true (x <=? x0)%positive) (CPToList (OCP cp)).
proof: Proof. intros cp. unfold OCP. unfold OCPAux. elim_eq_rect; simpl. rewrite CPLOK. apply StronglySorted_sort. intros x1 x2 x3. unfold is_true. intros Hx1x2 Hx2x3. apply Pos.leb_le in Hx1x2. apply Pos.leb_le in Hx2x3. apply Pos.leb_le. transitivity x2; assumption. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms