proposition: Lemma hamming_min_dist : min_dist hamming_not_trivial = 3%N.
proof: Proof. move: (min_dist_is_min hamming_not_trivial) => Hforall. move: (min_dist_achieved hamming_not_trivial) => Hexists. move: (min_dist_neq0) => H3. suff : min_dist hamming_not_trivial <> 1%N /\ min_dist hamming_not_trivial <> 2%N /\ min_dist hamming_not_trivial <= 3%N. move : H3. move/(_ _ _ _ hamming_not_trivial). destruct (min_dist hamming_not_trivial) as [|p]=> //. case: p Hforall Hexists => //; first by intuition. case; first by intuition. case; first by intuition. move=> p _ _ _ [_ [_ ]]; by case: p. split => [min1 | ]. case: Hexists => c [] Hc [] c0. rewrite min1 => /no_weight_1_cw; apply. move: Hc; by rewrite memv_ker lfunE /= => /eqP. split => [min2 | ]. case: Hexists => c [] Hc [] c0. rewrite min2 => /no_weight_2_cw; apply. move: Hc; by rewrite memv_ker lfunE /= => /eqP. move: (Hforall (rV_of_nat n (7 * 2 ^ (n - 3)))). have -> : wH (rV_of_nat n (7 * 2 ^ (n - 3))) = 3%N. by rewrite -wH_7_rev7 ?Hamming.two_len // wH_7 // Hamming.two_len. apply; first by rewrite memv_ker lfun_simp /= weight_3_cw. 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