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