proposition: Lemma flip_stable_mult : stable_mult flip.
proof: Proof. unfold flip, stable_mult, fmult; intros; simpl. assert (H:([1/2]* f true) <= ([1-] ([1/2]* f false))); auto. rewrite (Udistr_plus_left k _ _ H); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)