proposition: Lemma hamming_not_trivial : not_trivial (Hamming.code m).
proof: Proof. exists (rV_of_nat n (7 * 2 ^ (n - 3))). rewrite memv_ker lfunE /= weight_3_cw eqxx /=. apply/eqP/rV_of_nat_neq0 => //; [exact: rev7_neq0 | exact: rev7_ub (Hamming.two_len _)]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) mathcomp(Rstruct) realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming bigop_ext fdist proba channel channel_code decoding binary_symmetric_channel