proposition: Lemma jtype_entry_ub (V : P_ n ( A , B )) b : \sum_(a : A) (JType.f V) a b < n.+1.
proof: Proof. apply (@leq_ltn_trans (\sum_ (a : A) \sum_ (b : B) (JType.f V) a b)). - apply leq_sum => a _. by rewrite (bigD1 b) //= leq_addr. - case: V => c f Hf H /=. move/eqP in Hf. by rewrite Hf. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup perm) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy num_occ channel types