proposition: Lemma compare_spec : forall cp1 cp2, CompSpec eqST ltST cp1 cp2 (compareST cp1 cp2).
proof: Proof. intros cp1 cp2. unfold eqST, ltST, compareST. apply compareListSpec. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms