proposition: Lemma glb_eq_plus : forall (f g : natO-m>UI), glb ((Imon2 UPlus @2 f) g) == glb f + glb g.
proof: Proof. intros; apply Ueq_opp; apply Oeq_sym. apply (lub_comp2_eq (D1:=Uopp) (D2:=Uopp) (D3:=Uopp) (F:=Imon2 UPlus)) with (f:=f) (g:=g); intros. apply continuous_eq_compat with (Imon (UPlus k)); auto. apply continuous_eq_compat with (Imon2 UPlus); auto. Qed.
imports: ALEA(Utheory)