proposition: Lemma convexity w : p [~] q = (p <| w |> p) [~] (q <| w |> p) [~] (p <| w |> q) [~] (q <| w |> q).
proof: Proof. rewrite -[LHS](choicemm (probcplt w)). rewrite choiceDr. rewrite -[in RHS]altA altACA. rewrite -2![in RHS]choiceDr. by rewrite -2!choiceC. 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)