proposition: Lemma enc_pre_img_injective (P Q : P_ n ( A )) : enc_pre_img P != set0 -> enc_pre_img P = enc_pre_img Q -> forall a, type.d P a = type.d Q a.
proof: Proof. rewrite /enc_pre_img. case/set0Pn => m. rewrite in_set => HmP /setP HPQ. have HmQ : tuple_of_row (enc c m) \in T_{Q} by move:(HPQ m) ; rewrite 2!in_set => <-. move=> a {HPQ}. move: HmP ; rewrite in_set => /forallP/(_ a)/eqP => ->. move: HmQ ; rewrite in_set => /forallP/(_ a)/eqP => <-. reflexivity. 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