proposition: Lemma min_dist_double v w d m : f v = Some m -> w \in C -> dH w v <= d -> dH w m <= d.*2.
proof: Proof. move=> vm wC H. rewrite (leq_trans (dH_tri_ine v _ _)) // -addnn leq_add //. have {}wC : w \in [set cw in C] by rewrite inE. by rewrite dH_sym (leq_trans (MD_dec_f vm wC)). 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