proposition: Lemma mulnRdep_nz x y (Hx : x != O) : mulnRdep x y = x * y Hx.
proof: Proof. rewrite /mulnRdep /=. destruct boolP. by exfalso; rewrite i in Hx. do 2!f_equal; apply eq_irrelevance. 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