proposition: Lemma trivIset_shell : trivIset shell_partition.
proof: Proof. apply/trivIsetP => S1 S2; case/imsetP => V1 _ HS1; case/imsetP => V2 _ HS2 HS12. subst S1 S2. rewrite /disjoint. apply/pred0P => tb /=. apply/negP/negP. move: tb. apply/forallP; rewrite -negb_exists; apply/negP; case/existsP => tb /andP [H1 H2]; contradict HS12. apply/negP/negPn/eqP/setP => ?. rewrite 2!(@trivIset_shell' tb) //. exact: reflexive_relYn. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup perm) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy num_occ channel types