proposition: Lemma flip_stable_plus : stable_plus flip.
proof: Proof. unfold flip, stable_plus, fplus; intros; simpl. rewrite (Udistr_plus_left [1/2] _ _ (H true)). rewrite (Udistr_plus_left [1/2] _ _ (H false)). repeat norm_assoc_right. apply Uplus_eq_compat_right. repeat norm_assoc_left; apply Uplus_eq_compat_left; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)