proposition: Lemma zcard_rem i l : i != 0 -> i \in l -> i * (count_mem i l) * (zcard (rem i l)) = zcard l.
proof: Proof. move => Hi /perm_to_rem Hrem. have /zcard_any <- : sumn (rem i l) < (sumn l).+1. by rewrite ltnS (perm_sumn Hrem) /=; apply leq_addl. have Hil : i < (sumn l).+1. by rewrite ltnS (perm_sumn Hrem) /=; apply leq_addr. rewrite /zcard (perm_big _ Hrem) /= big_cons -!mulnA; congr (_ * _). rewrite mulnC -mulnA; congr (_ * _). rewrite [in RHS](bigD1 (Ordinal Hil)) //=. rewrite mulnC (seq.permP Hrem) /= eq_refl /= add1n. rewrite factS -!mulnA; congr (_ * _). rewrite [in LHS](bigD1 (Ordinal Hil)) //=; congr (_ * _). apply eq_bigr => j; rewrite -val_eqE => /= /negbTE Hij. move/seq.permP: Hrem => -> /=. by rewrite eq_sym Hij add0n. 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