proposition: Lemma merge_sort_sym : forall (hR1:transitive R) (hR2: antisymmetric R) (hR3: total R) (l1 l2:seq T), sorted R l1 -> sorted R l2 -> merge R l1 l2 = merge R l2 l1.
proof: Proof. move => hR1 hR2 hR3 l1 l2 h1 h2; apply (sorted_eq hR1 hR2). - by apply merge_sorted. - by apply merge_sorted. - by rewrite perm_merge perm_sym perm_merge perm_catC. Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)