proposition: Lemma pmf1_Pf : \sum_(m < Nmax.+1) \sum_(a in {: m.-tuple bool}) Pf a = 1.
proof: Proof. move: (uniq_dec_inj f_uniq) => f_inj. rewrite (_ : 1 = 1%mcR)// -(FDist.f1 P). rewrite (partition_big (inordf (size \o f)) (fun i => i \in 'I_Nmax.+1)) //=. apply: eq_bigr => i _. rewrite (big_seq_tuple i f_inj (fdist_card_neq0 P)) /Pf=>[|x]. apply: eq_big => x. apply/eqP/eqP => [H|<-]; first by apply: ord_inj; rewrite -H inordfE. by rewrite inordfE. by case: pickP => [? /eqP /f_inj ->| /(_ x)]; last rewrite eqxx. case: pickP => [? /eqP <-| _ ]; first by rewrite codom_f. by case: ifP. 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