proposition: Lemma decomp_codeword (c : 'rV[F]_n) : rVpoly c = rVpoly (low c) + rVpoly (high c) * 'X^d.
proof: Proof. rewrite poly_rV_K; last first. move: (@ltn_modp _ (rVpoly c) 'X^d). by rewrite size_polyXn -size_poly_eq0 size_polyXn. rewrite poly_rV_K; last first. rewrite size_divp; last by rewrite -size_poly_eq0 size_polyXn. rewrite size_polyXn /= -(subSn dn) (@leq_trans (n - d)) //. by rewrite leq_sub2r // size_poly. by rewrite addrC -divp_eq. 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