proposition: Lemma GRS_PCM_sq_vander (a b : 'rV[F]_n) (rn : r <= n) : GRS_PCM_sq a b r = vandermonde.Vandermonde r (\row_(i < r) a``_(inord i)) *m diag_mx (\row_(i < r) b``_(inord i)).
proof: Proof. apply/matrixP => i j. rewrite !mxE (bigID (fun i : 'I_n => i < r)) /=. rewrite [in X in _ + X = _](eq_bigr (fun=> 0)); last first. move=> l lr. rewrite !mxE (_ : l == inord j = false); last first. apply/negbTE; apply: contra lr => /eqP ->. by rewrite inordK // (leq_trans (ltn_ord j)). by rewrite mulr0n mulr0. rewrite big_const iter_addr0 addr0 big_ord_narrow //. apply/eq_bigr => l _. have Hl : widen_ord rn l = inord l. apply val_inj => /=; by rewrite inordK // (leq_trans (ltn_ord l)). rewrite !mxE Hl; congr (_ * (_ *+ _ )). rewrite (_ : inord j = widen_ord rn j) -?Hl //. apply val_inj => /=; by rewrite inordK //(leq_trans (ltn_ord j)). Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext vandermonde linearcode dft poly_decoding