proposition: Theorem IRcompose : forall xl xu yl yu zl zu : R, (-1 <= xl)%R -> (-1 <= yl)%R -> (zl <= xl + yl + xl * yl)%R -> (xu + yu + xu * yu <= zu)%R -> forall x y : R, (xl <= x <= xu)%R -> (yl <= y <= yu)%R -> (zl <= x + y + x * y <= zu)%R.
proof: Proof. intros xl xu yl yu zl zu Hx Hy Hzl Hzu x y (Hxl,Hxu) (Hyl,Hyu). replace (x + y + x * y)%R with ((1 + x) * (1 + y) - 1)%R. 2: ring. assert (H : (1 + zl <= (1 + x) * (1 + y) <= 1 + zu)%R). assert (H0 : (0 = 1 + -1)%R). ring. assert (Hc : forall a b : R, ((1 + a) * (1 + b) = 1 + (a + b + a * b))%R). intros a b. ring. assert (Hi : forall a b c : R, (a <= b)%R -> (b <= c)%R -> (1 + a <= 1 + b <= 1 + c)%R). intros a b c H1 H2. split. apply Rplus_le_compat_l with (1 := H1). apply Rplus_le_compat_l with (1 := H2). apply IRmult_pp with (1 + xl)%R (1 + xu)%R (1 + yl)%R (1 + yu)%R. rewrite H0. apply Rplus_le_compat_l with (1 := Hx). rewrite H0. apply Rplus_le_compat_l with (1 := Hy). rewrite Hc. apply Rplus_le_compat_l with (1 := Hzl). rewrite Hc. apply Rplus_le_compat_l with (1 := Hzu). apply Hi with (1 := Hxl) (2 := Hxu). apply Hi with (1 := Hyl) (2 := Hyu). assert (H0 : forall a : R, (a = (1 + a) + -1)%R). intros a. ring. split. rewrite (H0 zl). exact (Rplus_le_compat_r _ _ _ (proj1 H)). rewrite (H0 zu). exact (Rplus_le_compat_r _ _ _ (proj2 H)). Qed.
imports: Reals