proposition: Lemma leS_total : forall (S:osym_module), total (@leS S).
proof: Proof. rewrite /leS => S a b. rewrite cmpS_neg. by case: (cmpS b a). Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)