proposition: Lemma syndrome_hamming_err y : syndrome (Hamming.PCM m) (hamming_err y) = syndrome (Hamming.PCM m) y.
proof: Proof. rewrite /hamming_err. move Hs : (syndrome (Hamming.PCM m) y) => s. case/boolP : (s == 0) => [/eqP ->|s0]. by rewrite nat_of_rV_0 syndrome0. have [k ks] : exists k : 'I_n, nat_of_rV s = k.+1. move: s0; rewrite -nat_of_rV_eq0 -lt0n => s0. move: (nat_of_rV_up s) => sup. have sn1up : (nat_of_rV s).-1 < n. by rewrite /n Hamming.len_dim -ltnS prednK // prednK // expn_gt0. exists (Ordinal sn1up); by rewrite /= prednK. rewrite ks /= /syndrome. transitivity (col (Ordinal (rev_ord_proof (Ordinal (rev_ord_proof k)))) (Hamming.PCM m))^T. rewrite trmx_mul trmxK. rewrite (mulmx_rV_of_nat_row (Hamming.PCM m)^T (Ordinal (rev_ord_proof k))). by rewrite tr_col. rewrite col_matrix /= subnS prednK; last by rewrite subnBA // addnC addnK. by rewrite subnBA // addnC addnK -ks trmxK nat_of_rVK. 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