proposition: Lemma lub_inv : forall (f g : natO-m>U), (forall n, f n <= [1-] g n) -> lub f <= [1-] (lub g).
proof: Proof. intros; apply Uinv_le_perm_right. apply lub_le; intros. apply Uinv_le_perm_right. rewrite (lub_lift_left f n). apply lub_le; simpl; intros. apply Ole_trans with ([1-] (g (n+n0)%nat)); auto with arith. Qed.
imports: ALEA(Utheory)