proposition: Lemma lub_eq_plus : forall f g : natO-m>U, lub ((UPlus @2 f) g) == lub f + lub g.
proof: Proof. intros; apply Oeq_sym. apply lub_comp2_eq with (D1:=U) (D2:=U) (D3:=U) (F:=UPlus) (f:=f) (g:=g); auto. Qed.
imports: ALEA(Utheory)