proposition: Lemma converse_case1 : @E_leng_cw _ _ P f < n%:R * log #|A|%:R -> `H (P `^ n) <= @E_leng_cw _ _ P f + log ((exp 1) * n%:R * log #|A|%:R).
proof: Proof. move=>H. apply: (leR_trans (apply_le_HN_logE_loge (P `^ n) f_uniq)). rewrite leR_add2l; apply: Log_increasing_le => //. by apply/mulR_gt0; [exact/exp_pos | exact/EX_gt0]. by rewrite -mulRA; apply: leR_wpmul2l; [exact/ltRW/exp_pos|exact/ltRW]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code