proposition: Lemma Hr1 : 0 < (`H P - r) / 2.
proof: Proof. apply divR_gt0; last lra. by case: Hr => ? ?; lra. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep typ_seq source_code