proposition: Lemma no_failure_sup : #| no_failure |%:R <= exp2 (k.+1%:R * (`H P - e0)).
proof: Proof. apply (@leR_trans (exp2 n%:R)). rewrite /no_failure. have Hsubset : [set x | dec sc (enc sc x) == x] \subset dec sc @: (enc sc @: [set: 'rV[A]_k.+1]). apply/subsetP => x; rewrite inE => /eqP Hx. by apply/imsetP; exists (enc sc x) => //; rewrite imset_f. apply (@leR_trans #| dec sc @: (enc sc @: [set: 'rV[A]_k.+1]) |%:R). by apply/le_INR/leP; case/subset_leqif_cards : Hsubset. apply (@leR_trans #| dec sc @: [set: 'rV[bool]_n] |%:R). by apply/le_INR/leP/subset_leqif_cards/imsetS/subsetP => x Hx; rewrite inE. apply (@leR_trans #| [set: 'rV[bool]_n] |%:R). exact/le_INR/leP/leq_imset_card. rewrite cardsT card_mx /= card_bool natRexp2 mul1n. by apply/RleP; rewrite lexx. apply Exp_le_increasing => //. rewrite /e0 [X in _ <= _ * X](_ : _ = r); last by field. apply (@leR_pmul2r (1 / r)) => //. by apply divR_gt0; [lra | tauto]. rewrite -mulRA div1R mulRV ?mulR1; last first. by case: Hr => /RltP; rewrite lt0r => /andP[]. by case/leR_max : Hk. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep typ_seq source_code