proposition: Lemma reflexive_relYn ta : reflexive (relYn ta).
proof: Proof. rewrite /reflexive /relYn => tb. apply/forallP => a; apply/forallP => b; by rewrite eqxx. 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