proposition: Lemma non0_codeword_lowest_deg_uniq (g : 'rV['F_2]_n) : g \in C -> g != 0 -> codeword_lowest_deg C g -> forall j, j \in C -> j != 0 -> size (rVpoly g) = size (rVpoly j) -> g = j.
proof: Proof. move=> gC g0 Cg /= j jC j0 gj. set k : 'rV_n := g - j. apply/eqP; apply/negPn; apply/negP => abs. have gk : size (rVpoly g) <= size (rVpoly k). move: Cg. rewrite /codeword_lowest_deg => /forallP/(_ k)/implyP; apply. apply/and3P; split. - by rewrite /k (proj2 (Lcode0.aclosed C)) // Lcode0.oclosed. - apply: contra j0. by rewrite /k subr_eq addrC -subr_eq subrr eq_sym. - rewrite /k; move: abs; apply contra; by rewrite subr_eq0. suff kg : size (rVpoly k) < size (rVpoly g). by move: (leq_ltn_trans gk kg); rewrite ltnn. rewrite /k linearB /=; case/boolP: (1 < size (rVpoly g)) => size_1g. - apply: size_sub => //=; last by apply lead_coef_F2. apply/eqP; apply: contra g0; by rewrite rVpoly0. - rewrite -leqNgt in size_1g. have sz_g1 : size (rVpoly g) = 1%N. have : size (rVpoly g) != O by rewrite size_poly_eq0 rVpoly0. by case: (size _) size_1g => //; case. rewrite (@size1_polyC_F2 _ sz_g1). rewrite gj in sz_g1. by rewrite (@size1_polyC_F2 _ sz_g1) size_polyC subrr size_poly0. 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