proposition: Lemma perm_permutations s t : perm_eq s t -> perm_eq (permutations s) (permutations t).
proof: Proof. move=> Est; apply/uniq_perm; try exact: permutations_uniq. by move=> u; rewrite !mem_permutations (permPr Est). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)