proposition: Lemma lambda2_lt1 : lambda / 2 < 1.
proof: Proof. exact: (leR_ltR_trans lambda2_epsilon epsilon01.2). 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