proposition: Lemma card_ballE q n (r : nat) : r <= n -> prime q -> forall x : 'rV['F_q]_n, #| ball x r | = card_ball q n r.
proof: Proof. destruct q as [|q'] => //. destruct q' as [|q'] => //. set q := q'.+2. destruct n as [|n']. rewrite leqn0 => /eqP -> => primep x. rewrite (empty_rV x) /card_ball big_ord_recl bin0 mul1n big_ord0 addn0 expn0. rewrite /ball (_ : [set _ | _] = set1 0) ?cards1 //; apply/setP => /= y. by rewrite !inE leqn0 dH0x wH_eq0. set n := n'.+1. move=> rn primeq x. rewrite /ball. have -> : [set y | dH x y <= r] = \bigcup_(i < r.+1) [set y | dH x y == i]. apply/setP => /= y; rewrite !inE. apply/idP/bigcupP => [xy|]. rewrite -ltnS in xy. exists (Ordinal xy) => //; by rewrite inE. case=> /= i _. rewrite inE => /eqP ->. move: (ltn_ord i); by rewrite ltnS. transitivity (\sum_(i < r.+1) #| [set y | dH x y == i] |)%N. set D := \bigcup_(i < _) _. set f := fun i : 'I_r.+1 => [set y | dH x y == i]. have [H1 H2] : trivIset (f @: 'I_r.+1) /\ {in 'I_r.+1 &, injective f}. apply: trivIimset. - move=> i j _ _ ji; rewrite -setI_eq0; apply/eqP/setP => /= y. rewrite !inE. case/boolP : (dH x y == i) => //= /eqP ->. apply/negbTE; by rewrite eq_sym. - apply/negP; case/imsetP => /= i _ => /esym. apply/eqP/sphere_not_empty. rewrite (leq_trans _ rn) //; move: (ltn_ord i); by rewrite ltnS. have partD : partition (f @: enum 'I_r.+1) D. apply/and3P; split. - rewrite cover_imset //; apply/eqP/eq_bigl => i; by rewrite mem_enum. - rewrite (_ : [set f x | x in _ ] = [set f x | x : 'I_r.+1]) //. apply/setP => s; apply/imsetP/imsetP => -[a Ha ->]; first by exists a. exists a => //; by rewrite mem_enum. - apply/negP; case/imsetP => /= i _. apply/eqP; rewrite eq_sym; apply/sphere_not_empty. by rewrite (leq_trans _ rn) //; move: (ltn_ord i); rewrite ltnS. rewrite (card_partition partD) /= big_imset /=. - apply eq_bigl => i; by rewrite mem_enum. - move=> i j _ _;by apply H2. apply eq_bigr => i _. rewrite card_sphere // (leq_trans _ rn) //; move: (ltn_ord i); by rewrite ltnS. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector) ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code