proposition: Lemma sub_XrVpoly_rcs (R : idomainType) n (x : 'rV[R]_n.+1) : 'X * rVpoly x - rVpoly (rcs x) = (x 0 (inord n))%:P * ('X^n.+1 - 1).
proof: Proof. apply/polyP => i. rewrite coef_add_poly coefXM coefCM coef_add_poly coefXn 2!coef_opp_poly coefC. case: ifPn => [/eqP ->|i0]; last rewrite subr0. rewrite 2!add0r mulrN1 coef_rVpoly /=. case: insubP => //= j _ j0. rewrite mxE PermDef.fun_of_permE ffunE /= -val_eqE j0 /= j0 eqxx; congr (- x _ _). by apply val_inj => /=; rewrite inordK. case/boolP : (i == n.+1) => [/eqP ->|in0]. rewrite mulr1 2!coef_rVpoly /=. case: insubP => /= [j _ j0|]; last by rewrite ltnS leqnn. case: insubP => /= [?|_]; first by rewrite ltnn. rewrite subr0; congr (x _ _); apply val_inj => /=; by rewrite j0 inordK. rewrite mulr0 2!coef_rVpoly; case: insubP => /= [j|]. rewrite ltnS => in0' ji; case: insubP => /= [k _ ki|]. apply/eqP; rewrite subr_eq0; apply/eqP. rewrite mxE PermDef.fun_of_permE ffunE -val_eqE /= ki (negPf i0) -ji; congr (x _ _). apply/val_inj => /=; by rewrite inordK. rewrite ltnS -ltnNge => n0i; exfalso. rewrite -ltnS prednK // in in0'; last by rewrite lt0n. by move/negP : in0; apply; rewrite eq_sym eqn_leq {}n0i. rewrite -leqNgt => n0i; case: insubP => /= [j|]; last by rewrite subrr. rewrite ltnS => in0' ji; exfalso; move/negP : in0; apply. by rewrite eqn_leq ltnW //= (leq_trans n0i (leq_pred i)). 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