proposition: Lemma perm_map_inj s t : perm_eq (map f s) (map f t) -> perm_eq s t.
proof: Proof. move/permP=> Est; apply/allP=> x _ /=. have Dx: pred1 x =1 preim f (pred1 (f x)) by move=> y /=; rewrite inj_eq. by rewrite !(eq_count Dx) -!count_map Est. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)