proposition: Lemma szHs_is_nHs s (H : size s != O) : size s * `H (@num_occ_dist s H) = nHs s.
proof: Proof. rewrite /entropy /nHs /num_occ_dist /= -mulRN1 big_distrl big_distrr /=. apply eq_bigr => a _ /=; rewrite ffunE. case: ifPn => [/eqP -> | Hnum]; first by rewrite !mulRA !simplR. rewrite {1}/Rdiv (mulRC N(a | s)) 3![in LHS]mulRA mulRV ?INR_eq0' // ?mul1R. by rewrite -mulRA mulRN1 -logV ?Rinv_div//; apply divR_gt0; rewrite ltR0n lt0n. 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