proposition: Lemma Mdiv_stable_plus : forall A (k:U)(d:distr A), stable_plus (Mdiv k (mu d)).
proof: Proof. red; intros; repeat rewrite Mdiv_simpl. apply Oeq_trans with ((mu d f + mu d g)/k); auto. apply Udiv_eq_compat_left; auto. apply (mu_stable_plus d); trivial. Qed.
imports: ALEA(Monads) ALEA(Utheory)