proposition: Lemma Hdelta : 0 < delta.
proof: Proof. rewrite /delta. apply Rmin_pos. case: Hr => ? ?; apply divR_gt0; lra. apply divR_gt0; [exact lambda0 | 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