proposition: Lemma trivIset_enc_pre_img : trivIset enc_pre_img_partition.
proof: Proof. apply/trivIsetP => S1 S2 /imsetP ; case => P1 _ HP1. case/imsetP => P2 _ HP2 HP12. subst S1 S2. rewrite /disjoint. apply/pred0P => m /=. apply/negP/negP. move: m. apply/forallP; rewrite -negb_exists; apply/negP; case/existsP => m /andP [H1 H2]; contradict HP12. apply/negP/negPn/eqP/setP => m'. case/boolP : (m' \in enc_pre_img P2) => [|/negbTE] Hcase. - apply/negPn/negPn. rewrite 2!in_set; apply/forallP => a. move: H1; rewrite 2!in_set => /forallP/(_ a)/eqP ->. move: Hcase; rewrite 2!in_set => /forallP/(_ a)/eqP <-. move: H2; rewrite 2!in_set => /forallP/(_ a)/eqP <-. by rewrite eqxx. - apply/negP/negPn; move: Hcase => /negP/negPn; apply contra => Hcase. rewrite 2!in_set; apply/forallP => a. move: H2; rewrite 2!in_set => /forallP/(_ a)/eqP ->. move: Hcase; rewrite 2!in_set => /forallP/(_ a)/eqP <-. move: H1; rewrite 2!in_set => /forallP/(_ a)/eqP <-. by rewrite eqxx. 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