proposition: Lemma ctyp_element_ub : ((JType.f V) a b < N(a | ta).+1)%nat .
proof: Proof. by rewrite ltnS -(H Hta) (bigD1 b) // leq_addr. 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