proposition: Lemma choiceA_alternative {R : realType} (M : convexMonad R) : forall (T : UU0) (p q r s : {prob R}) (a b c : M T), (p = (r : R) * (s : R) :> R /\ (Prob.p s).~ = (Prob.p p).~ * (Prob.p q).~)%R -> let bc := choice q _ b c in let ab := choice r _ a b in choice p _ a bc = choice s _ ab c.
proof: Proof. move=> T p q r s a b c [Hp Hs] bc ab. rewrite choiceA// (_ : [s_of p, q] = s); last first. apply/val_inj => /=; rewrite s_of_pqE//. by move/(congr1 (@onem _)) : Hs; rewrite onemK. have [->|s0] := eqVneq s 0%:pr; first by rewrite !choice0. rewrite (_ : [r_of p, q] = r)//. apply/val_inj => /=. rewrite r_of_pqE s_of_pqE. move/(congr1 (@onem _)) : Hs; rewrite onemK => <-. rewrite Hp. by rewrite -GRing.mulrA GRing.divff// GRing.mulr1. 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)