proposition: Lemma Mchoice_continuous : forall (A:Type) (p:U), continuous2 (D1:=cDistr A) (D2:=cDistr A) (D3:=cDistr A) (MChoice A p).
proof: Proof. intros; apply continuous_continuous2; intros. apply (Mchoice_continuous_right (A:=A) p). apply (Mchoice_continuous_left (A:=A) p). Qed.
imports: ALEA(Probas) ALEA(Utheory)