proposition: Lemma ok_mult : forall (A:Type)(k p:U)(e:Distr A)(f : A -o> U), ok p e f -> ok (k*p) e (fmult k f).
proof: Proof. unfold ok; intros A k p e f oka. rewrite (mu_stable_mult e k f). apply Umult_le_compat_right; trivial. Qed.
imports: ALEA(Probas) ALEA(Utheory)