proposition: Lemma size_is_cgen g : g \in 'cgen -> size (rVpoly g) <= n.
proof: Proof. by rewrite 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