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