proposition: Lemma wH_hamming_err_ub y : wH (hamming_err y) <= 1.
proof: Proof. rewrite /hamming_err. move Hy : (nat_of_rV _) => [|p /=]. by rewrite (@leq_trans O) // eq_leq // wH0. by rewrite eq_leq // wH_two_pow // /n subSS sub_ord_proof. 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