proposition: Lemma card_typed_tuples_alt : INR #| T_{P} | <= exp2 (INR n * `H P).
proof: Proof. apply (@leR_trans (INR #| `TS P n 0 |)). apply/le_INR/leP. apply: leq_trans; last first. by apply subset_leq_card; exact: typed_tuples_are_typ_seq. by rewrite card_imset //; exact: row_of_tuple_inj. apply: (leR_trans (TS_sup _ _ _)); rewrite addR0. by apply/RleP; rewrite Order.POrderTheory.lexx. 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