proposition: Lemma choiceC A p (x y : gcm A) : x <|p|> y = y <|(Prob.p p).~%:pr|> x.
proof: Proof. by rewrite convC. Qed.
imports: Reals mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(boolp classical_sets) mathcomp(reals Rstruct) infotheo(classical_sets_ext Reals_ext ssrR fdist) infotheo(ssrR Reals_ext proba) infotheo(Reals_ext realType_ext) infotheo(fsdist convex necset) HB(structures) monae_lib hierarchy monad_lib proba_lib monad_model gcm_model category