proposition: Lemma monty_stick : play_n stick = bcoin (/ 3)%coqR%:pr.
proof: Proof. rewrite /play_n /monty /stick. transitivity (hide_n >>= (fun h => (pick def : M _) >>= (fun p => tease_n h p >> Ret (p == h)))). by bind_ext => d; bind_ext => d'; under eq_bind do rewrite bindretf. transitivity (hide_n >>= (fun h => (pick def : M _) >>= (fun p => Ret (h == p)))). bind_ext => d; bind_ext => d'. by rewrite arbitrary_inde // 1?eq_sym // Set3.size_filter2. by rewrite hide_pick_nondeter uFFTE. 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