proposition: Lemma aep_bound_decreasing e e' : 0 < e' <= e -> aep_bound e <= aep_bound e'.
proof: Proof. case=> Oe' e'e. apply leR_wpmul2l; first exact: aep_sigma2_ge0. apply leR_inv => //; first exact/pow_lt. apply pow_incr => //; split; [exact/ltRW | exact/e'e ]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext bigop_ext ssralg_ext logb fdist proba entropy