proposition: Lemma hamming_bound q n (C : Lcode0.t [finFieldType of 'F_q] n) (C_not_trivial : not_trivial C) t (tn : t <= n) : prime q -> min_dist C_not_trivial = t.*2.+1 -> #| C | * card_ball q n t <= q^n.
proof: Proof. move=> primeq. destruct q as [|q'] => //. destruct q' as [|q'] => //. set q := q'.+2. move/min_dist_ball_disjoint => H. suff : \sum_(c in C) #|ball c t| <= q ^ n. rewrite (eq_bigr (fun c => card_ball q n t)); last first. rewrite /= => c cC; by rewrite card_ballE. by rewrite big_const iter_addn_0 mulnC. have -> : q ^ n = #| 'rV['F_q]_n |. by rewrite card_mx mul1n card_ord Fp_cast. set P : {set {set _}} := [set ball c t | c in C]. have trivIP : trivIset P. apply/trivIsetP => /= s1 s2 /imsetP[/= c1 c1C] -> /imsetP[/= c2 c2C] -> s1s2. rewrite -setI_eq0; apply/eqP/H => //. by apply: contra s1s2 => /eqP ->. have /card_partition : partition P (\bigcup_(c in C) ball c t). apply/and3P; split => //; first by rewrite cover_imset. apply/imsetP; case => /= x xC. move/setP/(_ x); by rewrite !inE dHE subrr wH0 leq0n. rewrite big_imset /=; last first. move=> c1 c2 c1C c2C. case/boolP : (c1 == c2) => [/eqP //|c1c2 abs]. move: (H _ _ c1C c2C c1c2). rewrite abs setIid => /setP/(_ c2). by rewrite !inE dHE subrr wH0 leq0n. move=> <-; apply subset_leq_card; apply/subsetP => x; by rewrite inE. 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