proposition: Lemma uniform_singl (M : probMonad real_realType) (A : Type) (def : A) h : size h = 1%nat -> uniform def h = Ret (head def h) :> M A.
proof: Proof. case: h => // h [|//] _. by rewrite uniform_cons uniform_nil (@choice_ext 1%:pr) ?choice1 //= invR1. 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)