proposition: Lemma syndrome_syndromep y : syndrome (PCM a n d) y = poly_rV \RSsynp_(rVexp a n, y, d).
proof: Proof. apply/rowP => i; rewrite !mxE /syndromep poly_def coef_sum. evar (tmp : 'I_d -> F); transitivity (\sum_j (tmp j)); last first. apply eq_bigr => /= j _. apply/esym; rewrite /fdcoor coefZ horner_poly big_distrl /= /tmp; reflexivity. rewrite {}/tmp (exchange_big_dep xpredT) //=; apply eq_bigr => j _; rewrite !mxE. have @i' : 'I_d. by apply (@Ordinal _ i); rewrite (leq_trans (ltn_ord i)). rewrite (bigD1 i') //= coefXn insubT //= => Hj. rewrite eqxx mulr1 (_ : Ordinal Hj = j); last by apply val_inj. rewrite mxE inordK; last by rewrite ltnS (leq_trans (ltn_ord i)). rewrite mulrC; apply/eqP. rewrite addrC -subr_eq subrr; apply/eqP/esym. rewrite big1 // => k ki'; rewrite coefXn (_ : (_ == _) = false) ?mulr0 //. by apply: contraNF ki'; rewrite -val_eqE /= eq_sym. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext poly_ext channel_code decoding linearcode hamming dft poly_decoding euclid grs cyclic_code