proposition: Lemma Udiv_continuous : forall (k:U), continuous (UDiv k).
proof: Proof. red; intros. rewrite UDiv_simpl. apply (Ueq_orc 0 k); auto; intros. rewrite Udiv_by_zero; auto. apply (excluded_middle (A:=forall n, h n <= k)); auto; intros. apply Umult_div_le_right; auto. rewrite Umult_sym. apply Ole_trans with (lub (UMult k @ (UDiv k @ h))); auto. apply lub_le_compat; intro n; simpl; auto. rewrite Umult_div; auto. assert (exc (fun n => k<=h n)). apply exc_intro_class; intros; apply H0; intros; auto. apply Ult_le; auto. apply H1; auto; intros. apply Ole_trans with (h x / k). rewrite (Udiv_le_one (h x) H); auto. apply le_lub with (f:=UDiv k @ h) (n:=x). Qed.
imports: ALEA(Utheory)