proposition: Lemma mddP x y : f y != None -> x \in C -> dH x y <= mdd_err_cor C_not_trivial -> f y = Some x.
proof: Proof. move=> dec_not_None mC enc_m_v. have [m0 Hm0] : exists m0, f y = Some m0. case: (f y) dec_not_None => [m0|] // _; by exists m0. case/boolP : (odd (min_dist C_not_trivial)) => [odd_d | even_d]. - rewrite (mdd_oddE odd_d) in enc_m_v. apply/eqP/negPn/negP => abs. have {}abs : m0 != x by apply: contra abs; rewrite Hm0 => /eqP ->. have : min_dist C_not_trivial <= (min_dist C_not_trivial)./2.*2. move: abs. rewrite eq_sym => /(min_dist_prop C_not_trivial)/leq_trans; apply => //. move/subsetP : f_img; apply. by rewrite inE; apply/existsP; exists y; apply/eqP. by rewrite (@min_dist_double y). by rewrite -{1}(odd_double_half (min_dist C_not_trivial)) odd_d ltnNge leqnn. - rewrite (mdd_evenE even_d) in enc_m_v. apply/eqP/negPn/negP => abs. have {}abs : m0 != x by apply: contra abs; rewrite Hm0 => /eqP ->. have : (min_dist C_not_trivial)./2 <= (min_dist C_not_trivial)./2 - 1. move: (odd_double_half (min_dist C_not_trivial)). rewrite -leq_double (negbTE even_d) /= add0n => ->. move: abs. rewrite eq_sym. move/(min_dist_prop C_not_trivial)/leq_trans; apply => //. move/subsetP: f_img; apply. by rewrite inE; apply/existsP; exists y; apply/eqP. by rewrite (@min_dist_double y). apply/negP. rewrite -ltnNge subn1 prednK // half_gt0 ltnNge; apply: contra even_d. rewrite leq_eqVlt => /orP[/eqP->//|]. by rewrite ltnS leqn0 => /eqP/min_dist_neq0. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector) ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code