proposition: Lemma zcard_nil : zcard [::] = 1.
proof: Proof. rewrite /zcard big_nil mul1n /= big_const fact0. by rewrite eq_cardT // size_enum_ord /= mul1n. 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