proposition: Lemma echa_ge0 (HM : (0 < #| M |)%nat) W (c : code) : 0 <= echa(W , c).
proof: Proof. apply/RleP/mulR_ge0. - apply divR_ge0; [exact/Rle_0_1| exact/ltR0n]. - by apply/RleP/sumr_ge0 => ? _; exact: sumr_ge0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) Reals_ext ssrR logb fdist proba channel