proposition: Lemma Lt_pos : 0 < IZR L_typ.
proof: Proof. apply: (Rlt_le_trans _ (INR n * (`H P + epsilon))); last exact: (proj1 (ceilP _)). rewrite -(mulR0 0). apply: (Rmult_le_0_lt_compat _ _ _ _ (Rle_refl _) (Rle_refl _)). - by apply: lt_0_INR; apply/ltP. - by apply(Rplus_le_lt_0_compat _ _ (entropy_ge0 P) eps_pos). Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq natbin source_code