proposition: Lemma lambda_gt0 : 0 < lambda.
proof: Proof. by apply Rmin_glb_lt;[move: Hr => ? ; lra|exact: epsilon01.1]. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrZ ssrR Reals_ext ssr_ext ssralg_ext logb natbin fdist proba entropy aep typ_seq source_code