proposition: Lemma dvdn_zcard_fact n (l : 'P_n) : zcard l %| n`!.
proof: Proof. pose l' := (CTpartn l). have -> : zcard l = zcard l' by rewrite cast_intpartnE /=. rewrite -(permCTP l') -(card_cent1_perm (permCT l')). rewrite -card_Sn -cardsT; apply cardSg. exact: subsetT. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action gproduct morphism) tools partition permcomp cycles cycletype