proposition: Lemma pgen_is_cgen (g : 'rV_n) (C_not_trivial : not_trivial C) : rVpoly g \in 'pgen[[set cw in C]] -> g \in 'cgen[C].
proof: Proof. move=> Hg. rewrite is_cgenE; apply/and3P => [:H1]; split. - abstract: H1. by move/forallP : Hg => /(_ g); rewrite inE => /eqP ->. - apply/eqP => abs. have {}Hg : forall p, p \in [set cw in C] -> p = 0. move=> p Hp. move/forallP : Hg => /(_ p); rewrite Hp => /eqP/esym. by rewrite abs linear0 dvd0p rVpoly0 => /eqP. case: C_not_trivial => x /andP[] xC. move: (Hg x) => /=; rewrite inE => /(_ xC) ->; by rewrite eqxx. - apply/forallP => /= x; apply/implyP => /and3P[K1 K2 K3]. have gn : size (rVpoly g) <= n by rewrite size_poly. rewrite (divides_lowest_size C_not_trivial gn Hg). by apply size_lowestP. 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