proposition: Lemma keimel_plotkin_instance : (forall T p, right_distributive (fun a b : M T => a [~] b) (fun a b => a <| p |> b)) -> p <| (/ 2)%:pr |> q = (p <| (/ 2)%:pr |> q) <| (/ 2)%:pr |> (p [~] q).
proof: Proof. move=> altDr. have altDl T r : left_distributive (fun a b : M T => a [~] b) (fun a b => a <| r |> b). by move=> a b c; rewrite altC altDr (altC a) (altC b). rewrite -[LHS](altmm (p <| (/ 2)%:pr |> q)). transitivity (((p [~] p) <| (/ 2)%:pr|> (q [~] p)) <| (/ 2)%:pr |> ((p [~] q) <| (/ 2)%:pr |> (q [~] q))). by rewrite altDr altDl altDl. rewrite 2!altmm (altC q). rewrite (choice_halfC (p [~] q)). rewrite choiceACA. by rewrite choicemm. 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)