proposition: Lemma fdcoor_rcs' (i : 'I_n) x : a ^+ n = 1 -> a ^+ i * x ^`_ i = 0 -> (rcs x) ^`_ i = 0.
proof: Proof. move=> an1. rewrite /fdcoor (@horner_coef_wide _ n); last by rewrite /rVpoly size_poly. rewrite big_distrr /=. rewrite (eq_bigr (fun i1 : 'I_ _ => (rVpoly x)`_i1 * a ^+ i ^+ i1.+1)); last first. move=> i1 _; rewrite mulrC -mulrA; congr (_ * _). by rewrite mxE -!exprM -exprD mulnS addnC. move=> x_RS. rewrite (@horner_coef_wide _ n); last by move: (size_rcs x); rewrite size_Xn_sub_1. rewrite -{}[RHS]x_RS rcs_rcs_poly; apply/esym. rewrite (reindex_onto (@rcs_perm n) (perm_inv (@rcs_perm n))) /=; last first. move=> i1 _; by rewrite permKV. rewrite (eq_bigl xpredT); last by move=> i1; rewrite permK eqxx. apply eq_bigr => i1 _. rewrite coef_rVpoly PermDef.fun_of_permE ffunE. case: ifPn => [/eqP ->|]. case: insubP => [j _ jn0|]; last by rewrite ltnS leqnn. rewrite /= in jn0. rewrite coef_rVpoly; case: insubP => // k _ k0. rewrite mxE rcs_poly_rcs ?rVpolyK; last by rewrite size_poly. rewrite coef_rVpoly_ord mxE PermDef.fun_of_permE ffunE -val_eqE k0 /= expr0 mulr1. by rewrite exprAC an1 expr1n mulr1; congr (x _ _); apply val_inj => /=. case: insubP => /= [j|]. rewrite ltnS => i1n0 ji1 i10; rewrite coef_rVpoly. case: insubP => /= [k|]. rewrite ltnS => i1n0' ki1. rewrite mxE rcs_poly_rcs ?rVpolyK; last by rewrite size_poly. rewrite coef_rVpoly_ord mxE PermDef.fun_of_permE ffunE -val_eqE [val k]/= ki1 val_eqE (negPf i10). rewrite inordK; last by rewrite ltnW // ltnS prednK // lt0n. rewrite prednK // ?lt0n //; congr (x _ _ * _). by apply/val_inj. by rewrite mxE. rewrite ltnS => /negP abs; exfalso; apply: abs; by rewrite -ltnS. move=> /negP abs i10; exfalso; apply abs; by rewrite ltnS inordK. 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