proposition: Lemma lub_lub_inv_le : forall f g :natO-m>U, (forall n, f n <= [1-]g n) -> lub f <= [1-] lub g.
proof: Proof. intros; apply Ole_trans with (glb (UInvopp @ g)). apply lub_glb_le; auto. unfold glb; apply Uinv_le_compat. apply lub_le_compat; auto. Qed.
imports: ALEA(Utheory)