proposition: Lemma Lnt_nonneg : 0 <= IZR L_not_typ.
proof: Proof. apply: (Rle_trans _ (log (INR #|[set: n.-tuple X]|))); last exact: (proj1 (ceilP _)). rewrite -(Log_1 2); apply: Log_increasing_le => //. rewrite cardsT card_tuple -natRexp. by apply: pow_R1_Rle; apply: fdist_support_LB. 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