proposition: Lemma wH_non_0_cw : wH non_0_cw != O.
proof: Proof. by rewrite /non_0_cw; case/andP: (xchooseP C_not_trivial); rewrite wH_eq0. 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