proposition: Lemma choice_ext (q p : {prob real_realType}) (M : probMonad real_realType) A (m1 m2 : M A) : Prob.p p = Prob.p q :> R -> m1 <| p |> m2 = m1 <| q |> m2.
proof: Proof. by move/val_inj => ->. Qed.
imports: HB(structures) Reals Lra mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals mathcomp_extra Rstruct lra) infotheo(ssrR realType_ext Reals_ext) infotheo(proba convex necset) monae_lib hierarchy monad_lib fail_lib infotheo(fdist) mathcomp(reals Rstruct)