proposition: Lemma dim_hom_syndrome_ub : \dim (limg hom_syndrome) <= m.
proof: Proof. rewrite [in X in _ <= X](_ : m = \dim (fullv : {vspace 'rV[F]_m})); last first. by rewrite dimvf /Vector.dim /= mul1n. by rewrite dimvS // subvf. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector) ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code