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