proposition: Lemma play_strategy strategy : play strategy = (do hp <- uniform (def, def) (cp doors doors) ; let h := hp.1 in let p := hp.2 in do t <- tease h p ; do s <- strategy p t; Ret (s == h))%Do.
proof: Proof. rewrite -mpair_uniform; last 2 first. by rewrite /doors Set3.enumE. by rewrite /doors Set3.enumE. rewrite /play /monty /mpair bindA; bind_ext => x. rewrite bindA. by under [RHS]eq_bind do rewrite bindretf. 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