proposition: Lemma Mchoice_sym : forall (A:Type) (p:U) (m1 m2: Distr A), Mchoice p m1 m2 == Mchoice ([1-]p) m2 m1.
proof: Proof. intros; apply Ole_antisym; auto. apply Ole_trans with (Mchoice ([1-][1-]p) m1 m2); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)