proposition: Lemma success_factor_bound_part1 : success_factor tc V <= 1.
proof: Proof. apply/RleP; rewrite -(@ler_pM2l _ #|M|%:R)//; last by rewrite ltr0n. apply/RleP. rewrite /success_factor /Rdiv -(mulRC (/ #|M|%:R)%coqR) -!RmultE 2!mulRA. rewrite INRE mulRV; last first. by rewrite -INRE INR_eq0' -?lt0n. rewrite mul1R -INRE. rewrite -iter_addR -big_const /=. rewrite (_ : \sum_(m | m \in M ) 1 = \sum_(m : M) 1); last exact/eq_bigl. rewrite big_distrr /=. apply: leR_sumR => m _. rewrite mulNR exp2_Ropp. rewrite mulRC leR_pdivr_mulr // ?mul1R. apply/(@leR_trans #| V.-shell (tuple_of_row (enc tc m)) |%:R); last first. apply card_shelled_tuples => //. exact/typed_prop. case: (JType.c V) => _ Anot0. case/card_gt0P : (Anot0) => a _. exact: (fdist_card_neq0 (V a)). apply/le_INR/leP/subset_leq_card/setIidPl/setP => tb. by rewrite in_set in_set andbC andbA andbb. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext logb fdist entropy ln_facts num_occ types jtypes divergence conditional_divergence entropy channel_code channel