fact: Example gcmAP_choice_nontrivial (p q : {prob real_realType}) : p <> q -> Ret true <|p|> Ret false <> Ret true <|q|> Ret false :> (Monad_of_category_monad.acto Mgcm) bool.
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