proposition: Lemma neq0zcard n (l : 'P_n) : zcard l != 0.
proof: Proof. have:= dvdn_zcard_fact l; apply contraL => /eqP ->. by rewrite dvd0n -lt0n fact_gt0. 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