proposition: Lemma step3 : 1 - (esrc(P , sc)) <= \sum_(x in 'rV[A]_k.+1 | x \in ~: `TS P k.+1 delta) P `^ k.+1 x + \sum_(x in 'rV[A]_k.+1 | x \in no_failure :&: `TS P k.+1 delta) P `^ k.+1 x.
proof: Proof. rewrite step2; apply/leR_add2r/leR_sumRl => //= i Hi. by apply/RleP; rewrite lexx. by move: Hi; rewrite in_setI => /andP[]. 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