proposition: Lemma choicealtDr A (p : {prob real_realType}) : right_distributive (fun x y : Mgcm A => x <| p |> y) (@alt A).
proof: Proof. by move=> x y z; rewrite /choice lubDr. 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