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