proposition: Lemma Mchoice_continuous_left : forall (A:Type) (p:U), continuous (D1:=cDistr A) (D2:=cDistr A -M-> cDistr A) (MChoice A p).
proof: Proof. red; intros; intro m. rewrite (MChoice_simpl (A:=A) p). rewrite Mchoice_sym. apply Ole_trans with (lub (c:=cDistr A) ((MChoice A ([1-] p) m)@h)). apply (Mchoice_continuous_right ([1-]p) m h). rewrite fmon_lub_simpl. apply lub_le_compat; intros; intro f; simpl; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)