proposition: Lemma hide_pickE D (f : door -> door -> M D) : hide >>= (fun h => pick >>= f h) = uniform (def, def) (cp doors doors) >>= (fun hp => f hp.1 hp.2).
proof: Proof. transitivity (mpair (hide, pick) >>= (fun hp => f hp.1 hp.2)). rewrite bindA; bind_ext => x. by rewrite bindA; under [RHS]eq_bind do rewrite bindretf. by rewrite mpair_uniform // /doors Set3.enumE. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra reals Rstruct) infotheo(ssrR realType_ext Reals_ext proba) monae_lib hierarchy monad_lib fail_lib proba_lib