proposition: Lemma choiceA_compute {N : probMonad real_realType} (T F : bool) (f : bool -> N bool) : f T <|(/ 9)%:pr|> (f F <|(/ 8)%:pr|> (f F <|(/ 7)%:pr|> (f F <|(/ 6)%:pr|> (f T <|(/ 5)%:pr|> (f F <|(/ 4)%:pr|> (f F <|(/ 3)%:pr|> (f F <|(/ 2)%:pr|> f T))))))) = f F <|(/ 3)%:pr|> (f F <|(/ 2)%:pr|> f T) :> N _.
proof: Proof. have H27 : (0 <= (2/7 : R) <= 1)%mcR by apply/andP; split; lra. have H721 : (0 <= (7/21 : R) <= 1)%mcR by apply/andP; split; lra. have H2156 : (0 <= (21/56 : R) <= 1)%mcR by apply/andP; split; lra. have H25 : (0 <= (2/5 : R) <= 1)%mcR by apply/andP; split; lra. rewrite [in RHS](@choiceA_alternative _ _ _ _ _ (/ 2)%:pr (/ 3).~%:pr); last first. rewrite 3!probpK /= /onem. rewrite -!(RmultE,RminusE,R1E). split; field. rewrite choicemm. rewrite [in LHS](@choiceA_alternative _ _ _ (/ 3)%:pr (/ 2)%:pr (/ 2)%:pr (/ 3).~%:pr); last first. rewrite 3!probpK /= /onem. rewrite -!(RmultE,RminusE,R1E). split; field. rewrite choicemm. rewrite [in LHS](@choiceA_alternative _ _ _ (/ 4)%:pr (/ 3).~%:pr (/ 3)%:pr (/ 4).~%:pr); last first. rewrite 4!probpK /= /onem. rewrite -!(RmultE,RminusE,R1E). split; field. rewrite choicemm. rewrite [in LHS](@choiceA_alternative _ _ _ (/ 7)%:pr (/ 6)%:pr (/ 2)%:pr (@Prob.mk _ (2/7) H27)); last first. rewrite 4!probpK /= /onem; split. rewrite -RmultE -RdivE' -2!INRE !INR_IZR_INZ. field. rewrite -!(RmultE,RminusE). rewrite -RinvE'. rewrite (_ : 7%mcR = 7); last first. by rewrite -INRE !INR_IZR_INZ. rewrite (_ : 2%mcR = 2)//. rewrite -R1E. field. rewrite choicemm. rewrite [in LHS](@choiceA_alternative _ _ _ (/ 8)%:pr (@Prob.mk _ (2/7) H27) (@Prob.mk _ (7/21) H721) (@Prob.mk _ (21/56) H2156)); last first. rewrite probpK /= /onem; split. rewrite -RmultE -2!RdivE'. rewrite (_ : 21%mcR = 21); last first. by rewrite -INRE !INR_IZR_INZ. rewrite (_ : 56%mcR = 56); last first. by rewrite -INRE !INR_IZR_INZ. rewrite (_ : 7%mcR = 7); last first. by rewrite -INRE !INR_IZR_INZ. field. rewrite -2!RmultE -!RminusE -RdivE' -RinvE'. rewrite (_ : 56%mcR = 56); last first. by rewrite -INRE !INR_IZR_INZ. rewrite (_ : 7%mcR = 7); last first. by rewrite -INRE !INR_IZR_INZ. rewrite (_ : 21%mcR = 21); last first. by rewrite -INRE !INR_IZR_INZ. rewrite (_ : 2%mcR = 2); last first. by rewrite -INRE !INR_IZR_INZ. rewrite -R1E. field. rewrite (choiceC (/ 4).~%:pr). rewrite [in LHS](@choiceA_alternative _ _ _ (/ 5)%:pr (probcplt (/ 4).~%:pr) (/ 2)%:pr (@Prob.mk _ (2/5) H25)); last first. rewrite 3!probpK /= /onem; split. rewrite -2!RmultE -RinvE'. rewrite (_ : 2%mcR = 2); last first. by rewrite -INRE !INR_IZR_INZ. rewrite (_ : 5%mcR = 5); last first. by rewrite -INRE !INR_IZR_INZ. field. rewrite -!RmultE -!RminusE -RinvE'. rewrite (_ : 5%mcR = 5); last first. by rewrite -INRE !INR_IZR_INZ. rewrite (_ : 2%mcR = 2); last first. by rewrite -INRE !INR_IZR_INZ. rewrite -R1E. field. rewrite 2!choicemm. rewrite (choiceC (@Prob.mk _ (2/5) H25)). rewrite [in LHS](@choiceA_alternative _ _ _ (@Prob.mk _ (21/56) H2156) (probcplt (Prob.mk H25)) (/ 2)%:pr (/ 4).~%:pr); last first. rewrite 3!probpK /= /onem; split. rewrite -!RmultE -RminusE -RinvE'. rewrite (_ : 56%mcR = 56); last first. by rewrite -INRE !INR_IZR_INZ. rewrite (_ : 21%mcR = 21); last first. by rewrite -INRE !INR_IZR_INZ. rewrite -R1E. field. rewrite -!(RmultE,RminusE) -2!RinvE'. rewrite (_ : 56%mcR = 56); last first. by rewrite -INRE !INR_IZR_INZ. rewrite (_ : 21%mcR = 21); last first. by rewrite -INRE !INR_IZR_INZ. rewrite (_ : 5%mcR = 5); last first. by rewrite -INRE !INR_IZR_INZ. rewrite (_ : 2%mcR = 2); last first. by rewrite -INRE !INR_IZR_INZ. rewrite -R1E. field. rewrite choicemm. rewrite (choiceC (/ 4).~%:pr). rewrite [in LHS](@choiceA_alternative _ _ _ (/ 9)%:pr (probcplt (/ 4).~%:pr) (/ 3)%:pr (/ 3)%:pr); last first. rewrite 3!probpK /= /onem; split. rewrite -RmultE. field. rewrite -RmultE -!RminusE. rewrite -R1E. field. by rewrite choicemm choiceC. Qed.
imports: HB(structures) Reals Lra mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals mathcomp_extra Rstruct lra) infotheo(ssrR realType_ext Reals_ext) infotheo(proba convex necset) monae_lib hierarchy monad_lib fail_lib infotheo(fdist) mathcomp(reals Rstruct) infotheo(Reals_ext)