proposition: Lemma choice_halfC A (M : probMonad real_realType) (a b : M A) : a <| (/ 2)%:pr |> b = b <| (/ 2)%:pr |> a.
proof: Proof. rewrite choiceC (_ : (_.~)%:pr = (/ 2)%:pr) //. apply val_inj; rewrite /= /onem. rewrite -RminusE -R1E; field. 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)