proposition: Lemma random_continuous : forall n, continuous (random n).
proof: Proof. unfold continuous; intros; rewrite random_simpl. apply Ole_trans with (sigma (fun k : nat => lub (c:=U) (UMult ([1/]1+n) @ (h <o> k))) (S n)). apply sigma_le_compat; intros; simpl. rewrite (lub_eq_mult ([1/]1+n) (h <o> k)); auto. apply Ole_trans with (sigma (lub (c:=nat-O->U) (ford_shift (fun k : nat => (UMult ([1/]1+n) @ (h <o> k))))) (S n)); auto. rewrite sigma_lub1; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)