proposition: Lemma card_sphere q n k x : k <= n -> prime q -> #|[set a in 'rV['F_q]_n | dH x a == k]| = ('C(n, k) * q.-1 ^ k)%nat.
proof: Proof. move=> n0m0 primeq. rewrite /dH. transitivity (#|[set a in 'rV['F_q]_n | wH a == k]|). rewrite -!sum1dep_card (reindex_onto (fun y => x - y)%R (fun y => x - y)%R) /=; last first. by move=> y _; rewrite opprB addrCA subrr addr0. apply eq_bigl => y; by rewrite !opprB addrCA subrr addr0 eqxx andbT. destruct k as [|k]; last by apply: wH_m_card_gen. rewrite bin0 expn0 muln1. apply/eqP/cards1P; exists 0%R. apply/setP => i; by rewrite !inE wH_eq0. 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