proposition: Lemma monty_f_stick : play_f (@stick _) = Ret true <| (/ 3)%coqR%:pr |> (fail <| (/ 2)%coqR%:pr |> (Ret false : M _)).
proof: Proof. rewrite /play_f /monty hide_pickE. rewrite /stick. under eq_bind do rewrite bindretf tease_fE fun_if if_arg uniform_inde. Open (X in _ >>= X). transitivity (if x.1 == x.2 then Ret true else fail <| (/ 2)%coqR%:pr |> ret _ (head def (doors \\ [:: x.1; x.2])) >> Ret false : M _). case: ifPn => [/eqP <-|hp]; first by rewrite eqxx. by rewrite eq_sym (negbTE hp). reflexivity. under eq_bind do rewrite choice_bindDl bindfailf bindretf. rewrite (Set3.bcoin13E_pair _ def (fun b => if b then Ret true else fail <| (/ 2)%coqR%:pr |> Ret false : M _)) //. rewrite /bcoin. by rewrite choice_bindDl 2!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