proposition: Lemma ball_disjoint_min_dist_lb n q (C : Lcode0.t [finFieldType of 'F_q] n) (C_not_trivial : not_trivial C) t : (forall x y, x \in C -> y \in C -> x != y -> ball x t :&: ball y t = set0) -> forall x : 'rV_n, x \in C -> x != 0 -> t.*2 < wH x .
proof: Proof. move=> H x xC x0. rewrite ltnNge; apply: contra x0 => xt. apply/negPn/negP => x0. move: (H x 0 xC (mem0v C) x0) => {H}. apply/eqP/set0Pn => /=. case: (leqP (wH x) t) => H. by exists x; rewrite !inE dH0x H andbT dHE subrr wH0. set s := take t (enum (wH_supp x)). set x1 : 'rV['F_q]_n := vproj x [set i | i \in s]. exists x1; by rewrite !inE dH0x wH_vproj_take andbT wH_vproj_take2 // H. 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