proposition: Lemma permP s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2).
proof: Proof. apply: (iffP allP) => /= [eq_cnt1 a | eq_cnt x _]; last exact/eqP. have [n le_an] := ubnP (count a (s1 ++ s2)); elim: n => // n IHn in a le_an *. have [/eqP|] := posnP (count a (s1 ++ s2)). by rewrite count_cat addn_eq0; do 2!case: eqP => // ->. rewrite -has_count => /hasP[x s12x a_x]; pose a' := predD1 a x. have cnt_a' s: count a s = count_mem x s + count a' s. rewrite -count_predUI -[LHS]addn0 -(count_pred0 s). by congr (_ + _); apply: eq_count => y /=; case: eqP => // ->. rewrite !cnt_a' (eqnP (eq_cnt1 _ s12x)) (IHn a') // -ltnS. apply: leq_trans le_an. by rewrite ltnS cnt_a' -add1n leq_add2r -has_count has_pred1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)