proposition: Lemma Mchoice_continuous_right : forall (A:Type) (p:U) (m: Distr A), continuous (D1:=cDistr A) (D2:=cDistr A) (MChoice A p m).
proof: Proof. red; intros; intro f. rewrite (MChoice_simpl p m). rewrite (Mchoice_simpl p m). simpl mu at 2. rewrite lub_fun_eq. rewrite <- (lub_eq_mult ([1-]p) ((Mu A @ h) <_> f)). rewrite <- lub_eq_plus_cte_left; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)