proposition: Lemma set_typ_seq_incl (A : finType) (P : {fdist A}) n epsilon : 0 <= epsilon -> forall r, 1 <= r -> `TS P n (epsilon / 3) \subset `TS P n epsilon.
proof: Proof. move=> e0 r r1. apply/subsetP => /= x. rewrite !inE /typ_seq => /andP[/RleP H2 /RleP H3] [:Htmp]. apply/andP; split; apply/RleP. - apply/(leR_trans _ H2)/Exp_le_increasing => //. rewrite !mulNR leR_oppr oppRK; apply leR_wpmul2l; first exact/leR0n. apply/leR_add2l. abstract: Htmp. rewrite leR_pdivr_mulr; [apply leR_pmulr => //|]; lra. - apply/(leR_trans H3)/Exp_le_increasing => //. rewrite !mulNR leR_oppr oppRK; apply leR_wpmul2l; first exact/leR0n. apply leR_add2l; rewrite leR_oppr oppRK; exact Htmp. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep