proposition: Lemma no_0_type (A : finType) (d : {fdist A}) (t : {ffun A -> 'I_1}) : (forall a, d a = (t a)%:R / 0%:R) -> False.
proof: Proof. move=> H; apply R1_neq_R0. rewrite (_ : 1 = 1%mcR)//. rewrite -(FDist.f1 d). transitivity (\sum_(a | a \in A) INR (t a) / 0); first exact/eq_bigr. rewrite -big_distrl /= -big_morph_natRD. rewrite (_ : (\sum_(a in A) _)%nat = O) ?mul0R //. transitivity (\sum_(a in A) 0)%nat; first by apply eq_bigr => a _; rewrite (ord1 (t a)). by rewrite big_const iter_addn. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum perm) mathcomp(matrix) mathcomp(Rstruct) Reals ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist proba entropy num_occ channel_code channel typ_seq