proposition: Lemma comparison_negK : forall s t, s = CompOpp t -> t = CompOpp s.
proof: Proof. by case => [] []. Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)