proposition: Lemma size_rcs_poly (R : idomainType) n (x : {poly R}) (xn : size x <= n) : 0 < n -> size (rcs_poly x n) <= n.
proof: Proof. move=> n0. rewrite /rcs_poly. set xn1 := _ - _. apply (@leq_trans (size xn1).-1); last by rewrite /xn1 size_Xn_sub_1. rewrite -ltnS prednK; last by rewrite size_Xn_sub_1. have : xn1 != 0 by apply/monic_neq0/monic_Xn_sub_1. by move/ltn_modpN0; apply. 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