proposition: Lemma RS_message_size (p : 'rV_n) x : rVpoly p = x * \gen_(a, d) -> (size x).-1 <= n - d.+1.
proof: Proof. move=> Hx. case/boolP : (x == 0) => [/eqP ->|x0]; first by rewrite size_poly0. have : size (rVpoly p) <= n by rewrite size_poly. rewrite Hx size_mul // ?gen_neq0 // => H. rewrite -(leq_add2r d.+1) (subnK dn) (leq_trans _ H) //. rewrite -subn1 addnC addnBA; last by rewrite lt0n size_poly_eq0. by rewrite -subn1 addnC leq_sub2r // leq_add2l size_rs_gen. 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