proposition: Lemma lub_glb_le : forall (f:natO-m>U) (g:natO-m>UI), (forall n, f n <= g n) -> lub f <= glb g.
proof: Proof. intros; apply lub_le; intros. rewrite (glb_lift_left g n); auto. apply le_glb; simpl; intros. apply Ole_trans with (f (n+n0))%nat; auto with arith. Qed.
imports: ALEA(Utheory)