proposition: Lemma zcard_any l b : (sumn l < b) -> \prod_(i <- l) i * \prod_(i < b) (count_mem (i : nat) l)`! = zcard l.
proof: Proof. rewrite /zcard => /(big_ord_widen _ (fun i : nat => (count_mem i l)`!)) ->. congr (_ * _). rewrite (bigID (fun i : 'I_(_) => i < (sumn l).+1)) /=. rewrite -[RHS]muln1; congr (_ * _). apply big1 => i Hi. suff -> : count_mem (i : nat) l = 0 by rewrite fact0. apply /count_memPn; move: Hi; apply contra. rewrite ltnS => /perm_to_rem/perm_sumn -> /=. exact: leq_addr. 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