proposition: Lemma size_lowestP x : x \in C -> x != 0 -> lowest_size <= size (rVpoly x).
proof: Proof. move=> xC x0. rewrite /lowest_size. case: exists_non0_codeword_lowest_deg => g /= /and3P[H1 H2 /forallP]. move/(_ x); rewrite xC x0 /= andbT. case/boolP : (x == g) => [/eqP -> //| xg]. by rewrite 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