proposition: Lemma min_lub_le_incr_aux : forall f g : natO -m> U, (forall n, exc (fun m => (n<=m)%nat /\ f n <= g m)) -> min (lub f) (lub g) <= lub ((Min @2 f) g).
proof: Proof. intros; apply Ole_trans with (lub f); auto. apply lub_le; intros. apply (H n); auto; intros m (H1,H2). apply Ole_trans with (min (f m) (g m)); auto. apply min_le; auto. apply le_lub with (f:=(Min @2 f) g) (n:=m); simpl; auto. Qed.
imports: ALEA(Utheory)