proposition: Lemma Mdiv_stable_mult : forall A (k:U)(d:distr A)(dk : mu d (fone A) <= k), stable_mult (Mdiv k (mu d)).
proof: Proof. red; intros; repeat rewrite Mdiv_simpl. apply (Ueq_orc 0 k); auto; intros. repeat (rewrite Udiv_by_zero;auto). assert (forall f, mu d f <= k). intros; apply Ole_trans with (mu d (fone A)); auto. apply Oeq_trans with ((k0 * mu d f) / k); auto. apply Udiv_eq_compat_left; auto. apply (mu_stable_mult d); trivial. apply Umult_div_assoc; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)