fact: Record CodeRateType := mkCodeRateType { rate :> R ; _ : exists n d, (0 < n)%nat /\ (0 < d)%nat /\ rate = log (INR n) / INR d }.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) Reals_ext ssrR logb fdist proba channel