proposition: Lemma exists_non0_codeword_lowest_deg : { c : 'rV_n | non0_codeword_lowest_deg c }.
proof: Proof. apply: sigW. case: C_not_trivial => g /andP[gC g0]. have := erefl [arg min_(g' < g | (g' \in C) && (g' != 0)) (size (rVpoly g'))]. case: arg_minnP => /=; [by apply/andP | move=> g']. case/andP=> g'C g'0 g_min _. exists g'. rewrite /non0_codeword_lowest_deg g'C g'0 /= /codeword_lowest_deg. apply/forallP => y; apply/implyP => /and3P[yC yg' y0]. apply g_min; by rewrite yC. 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