proposition: Lemma min_dist_ball_disjoint n q (C : Lcode0.t [finFieldType of 'F_q] n) (C_not_trivial : not_trivial C) t : min_dist C_not_trivial = t.*2.+1 -> forall x y, x \in C -> y \in C -> x != y -> ball x t :&: ball y t = set0.
proof: Proof. move=> Hmin /= x y xC yC xy. apply/eqP/negPn/negP; case/set0Pn => /= z; rewrite !inE => /andP[xzt yzt]. have xyt : dH x y <= t.*2. by rewrite -addnn (leq_trans (dH_tri_ine z _ _)) // leq_add // dH_sym. move: (min_dist_prop C_not_trivial xC yC xy). rewrite Hmin => /(leq_ltn_trans xyt); by rewrite ltnn. 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