proposition: Lemma leS_antisym : forall (S: osym_module), antisymmetric (@leS S).
proof: Proof. rewrite /leS => S a b. rewrite cmpS_neg. case_eq (cmpS b a) => //=. move/eqP. move/cmpS_eq_axiom. by move => <-. Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)