proposition: Lemma szHs_is_nHs_full s : mulnRdep (size s) (fun H => Hs0 H) = nHs s.
proof: Proof. rewrite /mulnRdep; destruct boolP; last by apply szHs_is_nHs. rewrite /nHs (eq_bigr (fun a => 0)); first by rewrite big1. move=> a _; suff -> : N(a|s) == O by []. by rewrite /num_occ -leqn0 -(eqP i) count_size. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb fdist entropy convex ln_facts jensen num_occ