proposition: Lemma size_lowest g : non0_codeword_lowest_deg g -> size (rVpoly g) = lowest_size.
proof: Proof. case/and3P => gC g0 Hg. rewrite /lowest_size. case: exists_non0_codeword_lowest_deg => g' /= /and3P[g'C g'0 Hg']. case/boolP: (g == g') => [/eqP -> // | gg']. apply/eqP; rewrite eqn_leq. move: Hg => /forallP/(_ g'). rewrite g'C /= g'0 andbT eq_sym gg' implyTb => ->. move: Hg' => /forallP/(_ g). by rewrite gC /= g0 andbT gg' implyTb => ->. 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