proposition: Theorem IRplus : forall xl xu yl yu zl zu : R, (zl <= xl + yl)%R -> (xu + yu <= zu)%R -> forall x y : R, (xl <= x <= xu)%R -> (yl <= y <= yu)%R -> (zl <= x + y <= zu)%R.
proof: Proof. intros xl xu yl yu zl zu Hzl Hzu x y (Hxl,Hxu) (Hyl,Hyu). apply IRsubset with (1 := Hzl) (2 := Hzu). split. apply Rplus_le_compat with (1 := Hxl) (2 := Hyl). apply Rplus_le_compat with (1 := Hxu) (2 := Hyu). Qed.
imports: Reals