proposition: Lemma cover_enc_pre_img : cover enc_pre_img_partition = [set: M].
proof: Proof. rewrite /cover /enc_pre_img_partition. apply/setP => m. rewrite in_set. apply/bigcupP. exists (enc_pre_img (type_of_tuple (tuple_of_row (enc c m)))). - apply/imsetP; exists (type_of_tuple (tuple_of_row (enc c m))) => //. rewrite in_set. apply/andP; split => //. apply/set0Pn. exists m. rewrite 2!in_set. by apply/forallP => a; rewrite ffunE. - rewrite 2!in_set. by apply/forallP => a; rewrite ffunE. 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