proposition: Lemma source_direct_bound d D : { k | D <= (k.+1 * d.+1)%:R }.
proof: Proof. case: (source_direct_bound' d D) => k Hk. destruct k as [|k]; last by exists k. exists O; rewrite mul1n. by apply (@leR_trans 0%R); last exact: leR0n. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrZ ssrR Reals_ext ssr_ext ssralg_ext logb natbin fdist proba entropy aep typ_seq source_code