proposition: Lemma leS_trans : forall (S:osym_module), transitive (@leS S).
proof: Proof. rewrite /leS => S b a c. case_eq (cmpS a b) => // hc1 _. - case_eq (cmpS b c) => // hc2 _. by rewrite (cmpS_trans hc1 hc2). move/eqP: hc1. move/cmpS_eq_axiom. move => ->. by rewrite hc2. - case_eq (cmpS b c ) => // hc2 _. move/eqP: hc2. move/cmpS_eq_axiom. by move => <-; rewrite hc1. by rewrite (cmpS_trans hc1 hc2). Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)