proposition: Lemma echa_le1 (HM : (0 < #| M |)%nat) W (c : code) : echa(W , c) <= 1.
proof: Proof. rewrite /CodeErrRate div1R. apply/RleP/ (@leR_pmul2l (INR #|M|)); first exact/ltR0n. rewrite mulRA mulRV ?INR_eq0' -?lt0n // mul1R -iter_addR -big_const. by apply: leR_sumR => m _; exact: Pr_1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) Reals_ext ssrR logb fdist proba channel