proposition: Lemma remainder_in_code (c : {poly F}) (cn : size c <= n) : poly_rV c \in C -> forall p r, p \in C -> rVpoly p = rVpoly p %/ c * c + r -> size r < size c -> poly_rV r \in C.
proof: Proof. move=> cC p /= r p_in_C Hdivp_g Hsize_rem. have -> : r = `[ r ]_n. symmetry; rewrite modp_small //. apply (@ltn_trans (size c)) => //. by rewrite size_Xn_sub_1 // ltnS. rewrite (_ : r = rVpoly p - rVpoly p %/ c * c); last first. by rewrite {1}Hdivp_g addrAC subrr add0r. rewrite modpD linearD /=. have -> : `[ rVpoly p ]_n = rVpoly p. by rewrite modp_small // size_Xn_sub_1 // ltnS size_poly. rewrite rVpolyK; apply Lcode0.aclosed => //. by rewrite -mulNr shift_linearity_codeword. 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