proposition: Lemma ML_err_rate x1 x2 y : repair y = Some x1 -> x2 \in C -> W ``(y | x2) <= W ``(y | x1).
proof: Proof. move=> Hx1 Hx2. case/boolP : (W ``(y | x2) == 0) => [/eqP -> //| Hcase]. have PWy : receivable_prop P W y. apply/existsP; exists x2. by rewrite Hcase andbT fdist_uniform_supp_neq0 inE. case: (ML_dec (mkReceivable PWy)) => x' []. rewrite /= Hx1 => -[<-] ->. by apply: (le_bigmax_cond _ (fun i => W ``(y | i))). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup finalg perm) mathcomp(zmodp matrix vector order) mathcomp(lra mathcomp_extra Rstruct reals) Reals ssrR realType_ext Reals_ext ssr_ext ssralg_ext f2 fdist proba channel_code channel binary_symmetric_channel hamming pproba