proposition: Lemma trivIset_shell' tb tb' V : tb \in V.-shell ta -> tb' \in V.-shell ta = relYn ta tb' tb.
proof: Proof. rewrite 2!in_set => H. rewrite /relYn. apply eq_forallb => a; apply eq_forallb => b; move: H. by move/forallP/(_ a)/forallP/(_ b)/eqP => ->. 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