proposition: Lemma Rle0Pf' (m : 'I_Nmax.+1) : PN m <> 0 -> [forall a : m.-tuple bool, (0 <= Pf' m a)%mcR].
proof: Proof. move=> PNnon0; apply/forallPP; first by move=> ?; exact/RleP. move=> a; rewrite /Pf'. apply: (Rmult_le_reg_r (PN m)). move/eqP in PNnon0. by apply/RltP; rewrite lt0r PNnon0 ffunE; exact/RleP. rewrite mul0R ffunE /Rdiv -mulRA -Rinv_l_sym // mulR1 /Pf. by case: pickP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code