proposition: Lemma Imon2_plus_continuous : continuous2 (D1:=Uopp) (D2:=Uopp) (D3:=Uopp) (Imon2 UPlus).
proof: Proof. apply continuous_continuous2; red; intros. change (glb (Imon (UPlus k) @ h) <= k + glb h). rewrite glb_eq_plus_cte_left; trivial. intro y. change (glb (Imon (UPlus <_> y) @ h) <= glb h + y). rewrite glb_eq_plus_cte_right; trivial. Qed.
imports: ALEA(Utheory)