proposition: Lemma Uplus_opp_continuous_left : continuous (D1:=Uopp) (D2:=Uopp-M->Uopp) (Imon2 UPlus).
proof: Proof. red; intros. intro k; simpl. change (glb (Imon (UPlus <_> k) @ h) <= glb h +k). rewrite glb_eq_plus_cte_right; trivial. Qed.
imports: ALEA(Utheory)