proposition: Lemma lambda2_gt0 : 0 < lambda / 2.
proof: Proof. by apply divR_gt0 => //; exact: lambda_gt0. 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