proposition: Lemma perm_map s t : perm_eq s t -> perm_eq (map f s) (map f t).
proof: Proof. by move/permP=> Est; apply/permP=> a; rewrite !count_map Est. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)