proposition: Lemma mu_stable_div : forall (A:Type) (m:distr A)(k:U)(f : MF A), ~0==k -> f <= fcte A k -> mu m (fdiv k f) == mu m f / k.
proof: Proof. intros; apply Umult_div_eq; auto. rewrite Umult_sym. rewrite <- (mu_stable_mult m k). apply mu_stable_eq; simpl; apply ford_eq_intro; intro x. unfold fmult,fdiv; apply Umult_div; auto. apply (H0 x). Qed.
imports: ALEA(Monads) ALEA(Utheory)