proposition: Lemma discrete_continuous : forall A (c : nat -> U) (p : nat -> A), continuous (discrete c p).
proof: Proof. red; intros. rewrite discrete_simpl. apply Ole_trans with (serie (lub (c:=nat-O->U) (ford_shift (fun k => (UMult (c k) @ (h <o> (p k))))))). apply serie_le_compat; intro k. repeat rewrite fcpo_lub_simpl. apply (UMult_continuous_right (c k) (h <o> p k)). rewrite (serie_continuous (ford_shift (fun k : nat => UMult (c k) @ h <o> p k))). apply lub_le_compat; intro n; simpl; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)