proposition: Lemma play_stick : play stick = bcoin (/ 3)%coqR%:pr.
proof: Proof. rewrite {1}/play {1}/monty hide_pickE. transitivity (do hp <- uniform (def, def) (cp doors doors); let h := hp.1 in let p := hp.2 in do t <- tease h p ; Ret (p == h) : M _)%Do. bind_ext => x /=. by under eq_bind do rewrite bindretf. transitivity (uniform (def, def) (cp doors doors) >>= (fun hp => let h := hp.1 in let p := hp.2 in Ret (h == p)) : M _). bind_ext => -[x1 x2] /=. by rewrite /tease uniform_inde eq_sym. by rewrite Set3.bcoin13E_pair // bindmret. 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