proposition: Lemma min_lub_le : forall f g : natO-m>U, lub ((Min @2 f) g) <= min (lub f) (lub g).
proof: Proof. intros; apply min_le. apply lub_le. intro; apply Ole_trans with (f n); simpl; auto. apply lub_le. intro; apply Ole_trans with (g n); simpl; auto. Qed.
imports: ALEA(Utheory)