proposition: Lemma jtype_enumP A B n : Finite.axiom (@jtype_enum A B n).
proof: Proof. case=> d f Hf H /=. have : Finite.axiom (enum [finType of { f : {ffun A -> {ffun B -> 'I_n.+1}} | (\sum_(a in A) \sum_(b in B) f a b == n)%nat }]). rewrite enumT; by apply enumP. move/(_ (@exist _ _ f Hf)) => <-. rewrite /jtype_enum /=. rewrite /jtype_enum_f /=. destruct d as [d Anot0]. case/card_gt0P : (Anot0) => a _. move: (fdist_card_neq0 (d a)) => Bnot0. set tmp := pmap _ _. have -> : tmp = pmap (fun f => Some {| JType.c := chan_of_jtype Anot0 Bnot0 (sval f); JType.f := (sval f); JType.sum_f := proj2_sig f; JType.c_f := fun a b => eq_ind_r (eq^~ (if (\sum_(b0 in B) sval f a b0)%nat == 0%N then / #|B|%:R else (sval f a b)%:R / (\sum_(b0 in B) sval f a b0)%:R)) (erefl (if (\sum_(b0 in B) sval f a b0)%nat == 0%N then / #|B|%:R else (sval f a b)%:R / (\sum_(b0 in B) sval f a b0)%:R)) (ffunE (fun b0 : B => if (\sum_(b1 in B) sval f a b1)%nat == 0%N then / #|B|%:R else (sval f a b0)%:R / (\sum_(b1 in B) sval f a b1)%:R) b) |} ) (enum [finType of { f : {ffun A -> {ffun B -> 'I_n.+1}} | (\sum_(a in A) \sum_(b in B) f a b)%nat == n}]). apply: eq_pmap => V. destruct Sumbool.sumbool_of_bool; last by rewrite Anot0 in e. destruct Sumbool.sumbool_of_bool; last by rewrite Bnot0 in e0. congr Some. by apply/jtype_eqP => /=. rewrite count_map. by apply eq_count. 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