proposition: Lemma charac_bdist : {r : prob R | P = fdist_binary card_A r (Set2.a card_A)}.
proof: Proof. destruct P as [pf pf01]. have rb : 0 <= pf (Set2.b card_A) <= 1. move: (FDist.le1 (FDist.mk pf01) (Set2.b card_A)) => /= H1. by move: pf01 => /andP [/forallP pf0 _]; apply/andP. exists (Prob.mk rb). apply/fdist_ext => a /=. move: pf01 => /andP [/forallP pf0 /eqP pf1]. rewrite fdist_binaryE; case: ifPn => [/eqP -> |Ha/=]. by rewrite /onem -pf1 /= Set2sumE /= addrK. by move/Set2.neq_a_b/eqP : Ha <-. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext