proposition: Lemma card_Sn : #|'S_(n)| = n`!.
proof: Proof. rewrite (eq_card (B := perm_on [set : 'I_n])). by rewrite card_perm /= cardsE /= card_ord. move=> p; rewrite inE unfold_in /perm_on /=. by apply/esym/subsetP => i _; rewrite in_set. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)