proposition: Lemma Hlambdar : `H P + lambda <= r.
proof: Proof. rewrite /lambda. case: (Rlt_le_dec (r - `H P) epsilon) => ?. - rewrite Rmin_left; lra. - rewrite Rmin_right //; lra. 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