proposition: Lemma sum_messages_types' f : \sum_(P : P_ n ( A )) (\sum_(m |m \in enc_pre_img c P) f m) = \sum_ (S | S \in enc_pre_img_partition c) \sum_(m in S) f m.
proof: Proof. rewrite (bigID (fun P => [exists m, m \in enc_pre_img c P] )). rewrite (_ : forall a b, Radd_comoid a b = a + b) //. rewrite Rplus_comm big1 ; last first. move=> P ; rewrite andTb negb_exists => HP. apply big_pred0 => m /=. apply/negP/negPn; by move:HP => /forallP/(_ m) ->. rewrite /= add0R big_imset. apply eq_big => [P|P _] //=. rewrite in_set. case: set0Pn => [/existsP //| ?]; exact/existsP. move=> P Q; rewrite 2!in_set => HP HQ HPQ /=. move: (enc_pre_img_injective HP HPQ) => {HP HQ} {}HPQ. case: P HPQ => /= Pd Pf HP HPQ. case: Q HPQ => /= Qd Qf HQ HPQ. apply/type_eqP => /=. apply/eqP. apply ffunP => a. apply/val_inj/INR_eq. move: {HPQ}(HPQ a); rewrite HP HQ eqR_mul2r //. apply/invR_neq0; by rewrite INR_eq0. 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