proposition: Lemma scale_cgen (g' : 'rV[F]_n) (HC : not_trivial C) : g' \in 'cgen[C] -> { k | (k != 0) && (g' == k *: canonical_cgen HC) }.
proof: Proof. move=> Hg'. set g := canonical_cgen HC. case/boolP : (g == g') => [/eqP ->|gg']. exists 1; by rewrite scale1r oner_neq0 eqxx. have size_g := canonical_cgen_lowest_size HC. rewrite -/g in size_g. pose k := lead_coef (rVpoly g') / lead_coef (rVpoly g). pose g'' : {poly F} := rVpoly g' - k *: rVpoly g. have size_g' : size (rVpoly g') = size (rVpoly g) by rewrite size_g; apply size_lowest. case/boolP : (k == 0) => k0. exfalso. move: k0. rewrite /k mulf_eq0 invr_eq0 2!lead_coef_eq0. case/orP; rewrite rVpoly0; apply/negP. by case/and3P : Hg'. by case/and3P : (canonical_cgenP HC). have size_g'' : size g'' < size (rVpoly g). rewrite /g'' -size_g'; apply size_sub => //. apply/eqP; rewrite rVpoly0; by case/and3P : Hg'. rewrite lreg_size ?size_g' //; by apply/GRing.lregP. rewrite lead_coefZ /k -mulrA mulVr ?mulr1 // unitfE lead_coef_eq0 rVpoly0; by case/and3P : (canonical_cgenP HC). have g''C : poly_rV g'' \in C. rewrite /g'' linearD /= linearN /= linearZ /= (proj2 (Lcode0.aclosed C)) // ?rVpolyK; first by case/and3P : Hg'. rewrite Lcode0.oclosed // Lcode0.sclosed //; by case/and3P : (canonical_cgenP HC). have g''0 : g'' = 0. apply/eqP/negPn/negP => abs. case/and3P: (canonical_cgenP HC) => _ _ /forallP/(_ (poly_rV g'')). rewrite g''C /= -/g. have -> : poly_rV g'' != 0 :> 'rV_n. apply: contra abs => /poly_rV_0_inv; apply. rewrite /g'' ltnW //. have : size (rVpoly g') <= n by rewrite size_poly. apply/leq_trans/size_sub => //. apply/eqP; rewrite rVpoly0; by case/and3P : Hg'. rewrite lreg_size ?size_g' //; by apply/GRing.lregP. rewrite lead_coefZ /k -mulrA mulVr ?mulr1 // unitfE lead_coef_eq0 rVpoly0; by case/and3P : (canonical_cgenP HC). rewrite andbT poly_rV_K; last by rewrite ltnW // (leq_trans size_g'') // size_canonical_cgen. rewrite leq_eqVlt -(eq_sym (size g'')) ltn_eqF //=. apply/negP. rewrite negb_imply -leqNgt leq_eqVlt size_g'' orbT andbT. move: (size_g''). rewrite ltnNge; apply: contra => /eqP <-. rewrite poly_rV_K // ltnW //; apply: (leq_trans size_g''); by rewrite size_poly. rewrite /g'' in g''0. move/eqP : g''0; rewrite subr_eq add0r; move/eqP => g''0. exists k. by rewrite k0 -(rVpolyK g') g''0 linearZ /= rVpolyK. 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