proposition: Lemma alt_hamming_err_ub y : wH (alt_hamming_err y) <= 1.
proof: Proof. rewrite /alt_hamming_err. destruct (nat_of_rV _); first by rewrite wH0. clearbody n; clear. rewrite wH_sum. case/boolP : (n0 < n) => n0n. rewrite (bigD1 (Ordinal n0n)) //= mxE eqxx (eq_bigr (fun x => O)); last first. move=> i Hi; rewrite mxE ifF //. apply: contraNF Hi => /eqP Hi; by apply/eqP/val_inj. by rewrite big_const iter_addn mul0n. rewrite (eq_bigr (fun x => O)); first by rewrite big_const iter_addn. move=> i _; rewrite mxE ifF //=; by apply: contraNF n0n => /eqP ->. 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