proposition: Lemma uniform2 (M : probMonad real_realType) (A : Type) (def : A) a b : uniform def [:: a; b] = uniform def [:: b; a] :> M _.
proof: Proof. rewrite uniform_cons uniform_singl // uniform_cons uniform_singl //. set pa := Prob.mk _. rewrite choiceC /= (@choice_ext pa) //=. rewrite /onem -RminusE -R1E; field. 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) infotheo(Reals_ext)