proposition: Lemma choiceDl A p : left_distributive (fun x y : M A => x <| p |> y) (fun x y => x [~] y).
proof: Proof. by move=> x y z; rewrite !(choiceC p) choiceDr. 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)