proposition: Lemma sigma_continuous1 : continuous Sigma.
proof: Proof. red; intros; intro n. induction n; auto. change (tord natO) in n. apply Ole_trans with (sigma (lub h) (S n)); auto. rewrite sigma_S. apply Ole_trans with (lub h n + lub (Sigma @ h) n); auto. simpl lub. repeat (rewrite lub_fun_eq). apply Ole_trans with (lub ((UPlus @2 (h <o> n)) ((Sigma @ h) <_> n))); auto. Qed.
imports: ALEA(Utheory)