proposition: Lemma mu_stable_div_le : forall (A:Type) (m:distr A)(k:U)(f : MF A), ~0==k -> mu m (fdiv k f) <= mu m f / k.
proof: Proof. intros; apply Umult_div_le_left; auto. rewrite Umult_sym. rewrite <- (mu_stable_mult m k). apply mu_monotonic; intro x. unfold fmult,fdiv; apply Umult_div_le; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)