proposition: Lemma size_rcs_poly_old (R : idomainType) n (x : 'rV[R]_n) : size (rcs_poly (rVpoly x) n) <= n.
proof: Proof. destruct n as [|n']. rewrite /rcs_poly subrr modp0. have -> : x = 0 by apply/matrixP => i []. by rewrite linear0 mulr0 size_poly0. by rewrite size_rcs_poly // size_poly. 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