proposition: Lemma eqListSortOCP : forall (cp : tST), eqList (CPToList (OCP cp)) (PosSort.sort (CPToList cp)).
proof: Proof. intro cp. unfold OCP. unfold OCPAux. elim_eq_rect. simpl. rewrite CPLOK. apply eqListRefl. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms