proposition: Lemma Uplus_opp_continuous_right : forall k, continuous (D1:=Uopp) (D2:=Uopp) (Imon (UPlus k)).
proof: Proof. red; intros. change (glb (Imon (UPlus k) @ h) <= k + glb h). rewrite glb_eq_plus_cte_left; trivial. Qed.
imports: ALEA(Utheory)