proposition: Lemma coprime_errloc_erreval E : coprimep \sigma_(a, E) \omega_(f, a, E).
proof: Proof. apply/coprimepP => p p_sigma p_eta. suff no_root_p : forall x, root p x -> False. move : p_sigma; rewrite (decomp_errloc _ (proj2 Ha)) //. move/(dvdp_mull (\prod_(i in supp E) (- a ``_ i)^-1%:P)). rewrite mulrA -big_split /= (eq_bigr (fun=> 1%:P)); last first. move=> i _; by rewrite -polyCM mulVr // unitrN unitfE (proj2 Ha). rewrite big1 // mul1r -big_filter; case/dvdp_prod_XsubC => bs. set mask_bs := mask bs _. case size_bsE : (size mask_bs). move: size_bsE => /size0nil ->; by rewrite big_nil. have : 0 < size mask_bs by rewrite size_bsE. rewrite -has_predT => /hasP [/= i i_mask_bs] _ => p_prod. suff : root (\prod_(j <- mask_bs) ('X - (a ``_ j)^-1%:P)) (a ``_ i)^-1. rewrite -(eqp_root p_prod); by move/no_root_p. rewrite (@big_morph _ _ (fun p => root p (a ``_ i)^-1) false orb); last 2 first. move=> ? ?; by rewrite rootM. by apply/negP/negP/root1. rewrite big_has /=; apply/hasP; exists i => //; by rewrite root_XsubC. move=> x px. have [n0 [n0e xan0]] : exists n0, n0 \in supp E /\ x = (a ``_ n0)^-1. have : root \sigma_(a, E) x. rewrite -dvdp_XsubCl; apply: dvdp_trans p_sigma; by rewrite dvdp_XsubCl. rewrite /root (decomp_errloc _ (proj2 Ha)) hornerM mulf_eq0; case/orP. - rewrite horner_prod; case/prodf_eq0 => n0 n0e. by rewrite !hornerE oppr_eq0 (negPf (proj2 Ha n0)). - rewrite horner_prod; case/prodf_eq0 => n0 n0e. rewrite !hornerE subr_eq0 => /eqP ->; by exists n0. rewrite {x}xan0 in px. have {px} : root \omega_(f, a, E) (a ``_ n0)^-1. rewrite -dvdp_XsubCl; apply: dvdp_trans p_eta; by rewrite dvdp_XsubCl. rewrite /root horner_sum (bigD1 _ n0e) /=. set q := (X in _ + X == 0 -> _). have {q}-> : q = 0. rewrite {}/q (eq_bigr (fun=> 0)); first by rewrite big_const /= iter_addr0. move=> i /andP[ie in0]. rewrite !hornerE /= horner_prod (bigD1 n0) /=; last first. by rewrite in_setD1 n0e eq_sym andbT. by rewrite !hornerE /= divrr ?unitfE ?(proj2 Ha) // subrr mulr0 mul0r. rewrite addr0 !hornerE /= mulf_eq0; case/orP. - rewrite mulf_eq0 (negbTE (Hf _)) orbF. by move: n0e; rewrite inE /= => /negbTE ->. - by rewrite errloc_zero // in_setD1 eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft