proposition: Lemma lambda0 : 0 < lambda.
proof: Proof. by rewrite /lambda; apply Rmin_case => //; [exact Hepsilon1 | exact Hr1]. 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