proposition: Lemma wH_m_card_gen p n k : prime p -> k <= n -> #|[set a in 'rV['F_p]_n | wH a == k]| = ('C(n, k) * p.-1 ^ k)%N.
proof: Proof. move=> primep n0n. destruct p as [|p'] => //; destruct p' as [|p'] => //. set p := p'.+2. destruct k as [|k'] => //. rewrite bin0 expn0 mul1n. set s := [set _ in _ | _]. rewrite (_ : s = set1 0%R) ?cards1 //. apply/setP => /= x. by apply/idP/idP; rewrite !inE /= ?wH_eq0. set k := k'.+1. destruct n as [|n'] => //. set n := n'.+1. transitivity (#|[set a in 'rV['F_2]_n | wH a == k]| * p.-1 ^ k)%N; last first. by rewrite wH_m_card. rewrite -!sum1dep_card big_distrl /=. transitivity (\sum_(i : 'rV['F_2]_n | wH i == k) (\sum_(x : 'rV['F_p]_k | [forall j, x ``_ j != 0%R]) 1))%nat; last first. apply eq_bigr => x Hx. by rewrite card_rV_wo_zeros ?mul1n. rewrite exchange_big /=. set P := fun x : 'rV['F_p]_n => wH x == k. set Q := fun x : 'rV['F_p]_k => [forall j, x ``_ j != 0%R]. set f := fun x : 'rV['F_p]_n => (\row_i x ``_ (nth ord0 (enum (wH_supp x)) i) : 'rV['F_p]_k). rewrite (partition_big f Q) /=; last first. move=> /= x /eqP Hx. apply/forallP => /= i; by rewrite !mxE (@nth_wH_supp k). apply eq_bigr => x Hx. rewrite !sum1dep_card. set h : 'rV['F_p]_n -> 'rV['F_2]_n := fun y => \row_i (if y ``_ i != 0 then 1 else 0)%R. set h' : 'rV['F_2]_n -> 'rV['F_p]_n := fun y => \row_i if y ``_ i == 0%R then 0%R else x ``_ (inord (index i (enum (wH_supp y)))). apply esym. have Hh' : {in [set x0 | wH x0 == k] &, injective h'}. move=> u v Hu Hv. rewrite /h' => uv. apply/rowP => i. move/rowP: uv => /(_ i). rewrite !mxE. case: ifPn => u0i. case: ifPn => v0i; first by rewrite (eqP u0i) (eqP v0i). move/esym/eqP. set j := inord _. move/forallP in Hx. by move: (Hx j) => /negbTE ->. case: ifPn => v0i. set j := inord _. move/eqP. move/forallP in Hx. move: (Hx j); by move/negbTE ->. rewrite -2!f2.F2_eq1 in u0i, v0i. by rewrite (eqP u0i) (eqP v0i). rewrite -[in LHS](card_in_imset Hh'). apply eq_card => /= y. rewrite !inE. apply/imsetP/andP => /=. case=> z. have wH_h' : wH z = wH (h' z). rewrite /wH !count_map; apply eq_in_count => /= i _. rewrite !mxE. case: ifPn => //= zi0; apply/esym. set j := inord _. by move/forallP : Hx => /(_ j). rewrite inE => Hz ->; split; first by rewrite -wH_h'. apply/eqP/rowP => i. rewrite !mxE. move/eqP in Hz. have wH_supp_h' : wH_supp (h' z) = (wH_supp z). apply/setP => j. rewrite !inE !mxE; case: ifPn => // zj0 /=. move/forallP : Hx; by apply. case: ifPn => Kz. move: (@nth_wH_supp _ _ _ z n0n Hz). rewrite -wH_supp_h'. move/(_ i (ltn_ord i)); by rewrite Kz. rewrite wH_supp_h' index_uniq ?enum_uniq //. by rewrite inord_val. by rewrite -cardE card_wH_supp Hz. have wH_supp_h : wH_supp y = wH_supp (h y). apply/setP => j; rewrite !inE !mxE; by case: ifPn. case=> Hyn0 hyx. exists (h y); first by rewrite inE -card_wH_supp -wH_supp_h card_wH_supp. apply/rowP => i. rewrite !mxE. case: ifPn; first by case: ifPn => //; rewrite negbK => /eqP. case: ifPn => // yi0 _. rewrite -(eqP hyx) !mxE. have Hk : k = size (enum (wH_supp y)). rewrite -cardE; apply/esym; rewrite card_wH_supp; by apply/eqP. rewrite inordK; last by rewrite -wH_supp_h -/k Hk index_mem mem_enum inE. by rewrite wH_supp_h nth_index // mem_enum -wH_supp_h inE. Qed.
imports: Reals mathcomp(all_ssreflect fingroup zmodp ssralg finalg perm matrix) mathcomp(poly mxalgebra mxpoly) mathcomp(Rstruct) ssr_ext ssralg_ext f2 num_occ natbin ssrR Reals_ext bigop_ext