proposition: Lemma serie_continuous : continuous Serie.
proof: Proof. red; intros; rewrite Serie_simpl; unfold serie. apply Ole_trans with (lub (lub (Sigma @ h))). apply lub_le_compat; intro n; auto. apply sigma_continuous1. rewrite <- (lub_exch_eq (Sigma @ h)). apply lub_le_compat; intro n; auto. Qed.
imports: ALEA(Utheory)