proposition: Lemma min_lub_le_incr : forall f g : natO -m> U, min (lub f) (lub g) <= lub ((Min @2 f) g).
proof: Proof. intros f g; apply (incr_decomp f g); auto; intros. apply (min_lub_le_incr_aux f g); auto. rewrite min_sym. apply Ole_trans with (lub ((Min @2 g) f)); auto. apply (min_lub_le_incr_aux g f); auto. Qed.
imports: ALEA(Utheory)