proposition: Lemma mu_cte : forall (A : Type)(m:(distr A)) (c:U), mu m (fcte A c) == c * mu m (fone A).
proof: Proof. intros. apply Oeq_trans with (mu m (fun x => c * 1)). apply (mu_stable_eq m); simpl; auto. unfold fone; rewrite <- (mu_stable_mult m c (fun x => 1)); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)