proposition: Lemma star_continuous : forall (A B : Type) (m : M A)(F: A -> M B), continuous m -> (forall x, continuous (F x)) -> continuous (star m F).
proof: Proof. red; intros; simpl. apply Ole_trans with (m (fun x => lub (F x @ h))). apply (fmonotonic m); intro x. apply (H0 x h); auto. apply Ole_trans with (m (lub (c:=A-O->U) (ford_shift F @ h))); auto. apply Ole_trans with (1:=H (ford_shift F @ h)); auto. Qed.
imports: ALEA(Uprop) ALEA(Utheory)