proposition: Lemma scha_pos (W : `Ch(A, B)) (c : code) : 0 <= scha(W, c).
proof: Proof. by rewrite /scha; rewrite subr_ge0; exact/echa_le1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) Reals_ext ssrR logb fdist proba channel