proposition: Lemma canonical_cgenP : non0_codeword_lowest_deg C canonical_cgen.
proof: Proof. rewrite /canonical_cgen; by case: exists_non0_codeword_lowest_deg. 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