proposition: Lemma weight_3_cw : syndrome H (rV_of_nat n (7 * 2 ^ (n - 3))) = 0.
proof: Proof. have two_m := Hamming.two_len m'. apply/rowP => x; rewrite !mxE. have Hn' : size (bitseq_of_N (bin_of_nat (7 * 2 ^ (n - 3)))) = n. apply/eqP. rewrite eqn_leq size_bitseq_of_N_ub /=; last 2 first. exact/rev7_neq0. exact/rev7_ub. move: (@size_bitseq_of_N_lb (7 * 2 ^ (n - 3)) n.-1 (rev7_lb two_m)). by rewrite -ltnS prednK. rewrite (bigD1 0) //= !mxE. set i := nth _ _ 0. have {i} -> : i = true. rewrite /i /bitseq_of_nat /pad_seqL size_rev Hn'. by rewrite leqnn subnn cat0s bin_of_nat_rev7 // rev7_bin. rewrite mulr1. pose i1 := Ordinal (ltnW two_m); pose i2 := Ordinal two_m. rewrite (bigD1 i1) // (bigD1 i2) //= !mxE. set i := nth _ _ i1. have {i} -> : i = true. rewrite /i /bitseq_of_nat /pad_seqL size_rev Hn'. by rewrite leqnn subnn cat0s bin_of_nat_rev7 // rev7_bin. rewrite mulr1. set i := nth _ _ i2. have {i} -> : i = true. rewrite /i /bitseq_of_nat /pad_seqL size_rev Hn'. by rewrite leqnn subnn cat0s bin_of_nat_rev7 // rev7_bin. rewrite mulr1 big1 ?addr0 => [|i i_gt2]; last first. rewrite /rV_of_nat /bitseq_of_nat. rewrite !mxE /= /pad_seqL size_rev Hn' leqnn subnn /=. rewrite bin_of_nat_rev7 //= rev7_bin //=. set j := nth _ _ i. suff -> : j = false by rewrite mulr0. rewrite /j. clear -i_gt2. case: i i_gt2 => -[//|[//|[//|m0]]] /=. by rewrite nth_nseq ltn_subRL addnC addn3 => ->. rewrite /bitseq_of_nat. destruct x as [x Hx] => /=. set p0 := pad_seqL _ _ _. set p1 := pad_seqL _ _ _. set p2 := pad_seqL _ _ _. have [X|[X|X]] : (x = m.-1 \/ x = m.-2 \/ x < m.-2)%N. move: Hx; rewrite ltnS leq_eqVlt => /orP[/eqP ->|]; first by auto. by rewrite ltnS leq_eqVlt => /orP[/eqP|]; auto. - rewrite X. rewrite {1}(_ : m = size p0); last by rewrite /p0 size_pad_seqL. rewrite {1}(_ : m = size p1); last by rewrite /p0 size_pad_seqL. rewrite {1}(_ : m = size p2); last by rewrite /p0 size_pad_seqL. by rewrite 3!nth_last last_cat /= /p1 /p2 /= 2!last_cat /= add0r addrr_char2. - rewrite X /= /p0 /pad_seqL /=. rewrite -cat1s catA nth_cat /= size_nseq /= ltnS leqnn. rewrite (_ : false :: _ = nseq m'.+1 false) // nth_nseq ltnS leqnn /=. rewrite /p1 /pad_seqL /= nth_cat size_nseq subn2 ltnn subnn /=. rewrite /p2 /pad_seqL /= nth_cat size_nseq subn2 ltnn subnn /=. by rewrite addrr_char2 // addr0. - rewrite /p0 /p1 /p2 /= /pad_seqL /=. rewrite -cat_cons -[_::_]/(nseq _.+1 _) cats1 nth_rcons size_nseq ltnW // nth_nseq ltnW //. rewrite nth_cat size_nseq subn2 X /= nth_nseq X /=. by rewrite nth_cat size_nseq X /= nth_nseq X /= !addr0. 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