proposition: Lemma mddP' w v : f (w + v) != None -> w \in C -> wH v <= mdd_err_cor C_not_trivial -> f (w + v) = Some w.
proof: Proof. move=> wv wC Hv. suff ? : dH w (w + v) <= mdd_err_cor C_not_trivial by rewrite (@mddP w _). by rewrite /dH opprD addrA subrr sub0r wH_opp. 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