fact: Definition compareST (cp1 cp2 : tST) := compareList (PosSort.sort (CPToList cp1)) (PosSort.sort (CPToList cp2)).
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms