proposition: Lemma divides_lowest_size (HC : not_trivial C) (g : {poly F}) (gn : size g <= n) : g \in 'pgen[[set cw in C]] -> size g = lowest_size HC.
proof: Proof. move=> H. rewrite -(poly_rV_K gn). apply/size_lowest/and3P; split. - move/forallP : H => /(_ (poly_rV g)). rewrite inE => /eqP ->. by rewrite poly_rV_K. - apply/eqP => abs. have {}H : forall p, p \in [set cw in C] -> p = 0. move=> p Hp. move/forallP : H => /(_ p). rewrite Hp => /eqP/esym. by rewrite -(poly_rV_K gn) abs linear0 dvd0p rVpoly0 => /eqP. case: HC => x /andP [xC]. apply/negP; rewrite negbK; apply/eqP/H; by rewrite inE. - apply/forallP => /= x; apply/implyP => /and3P[H1 H2 H3]. rewrite poly_rV_K //. move/forallP : H => /(_ x); rewrite inE H1 => /eqP/esym. apply: dvdp_leq; by rewrite rVpoly0. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly polydiv vector) ssralg_ext poly_ext f2 hamming linearcode dft