proposition: Lemma cmpS_trans : forall (S:osym_module) (a b c:S) (x: comparison), cmpS a b = x -> cmpS b c = x -> cmpS a c = x.
proof: Proof. move => S a b c x. rewrite /cmpS => h1 h2. by apply (@cmp_trans _ _ a b c). Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)