proposition: Lemma tool_normP_in : forall (hd:T) tl l, perm_eq (hd::tl) l -> exists l1, exists l2, l = l1 ++ hd :: l2 /\ tl =i l1 ++ l2.
proof: Proof. move => hd tl l hp. have hs: (splitr hd l). - apply: splitPr. rewrite -(perm_mem hp). by rewrite in_cons eq_refl. case: hs hp => l1 l2 hp. exists l1; exists l2; split => //. apply: perm_mem. move: hp. by rewrite -[hd :: l2]cat1s perm_sym perm_catCA /= perm_cons perm_sym. Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)