proposition: Lemma Mmult_continuous : forall A (k:MF A) (d:distr A), continuous (Mmult k (mu d)).
proof: Proof. red; intros; simpl. apply Ole_trans with (mu d (fun (x:A) => lub (UMult (k x) @ (h <o> x)))). apply (mu_monotonic d); intros x; auto. rewrite (mu_continuous d (ford_shift (fun x => UMult (k x) @ h <o> x))). apply lub_le_compat; intro n; simpl; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)