proposition: Lemma choice0 {R : realType} (M : convexMonad R) (T : UU0) (a b : M T) : a <| 0%:pr |> b = b.
proof: Proof. rewrite choiceC/= [X in _ <| X |> _](_ : _ = 1%:pr) ?choice1//; apply/val_inj => /=. by rewrite mathcomp_extra.onem0. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra Rstruct reals) infotheo(Reals_ext) infotheo(realType_ext) monae_lib HB(structures) infotheo(convex)