proposition: Theorem IRmult_pp : forall xl xu yl yu zl zu : R, (0 <= xl)%R -> (0 <= yl)%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 Hx Hy Hzl Hzu x y (Hxl,Hxu) (Hyl,Hyu). apply IRsubset with (1 := Hzl) (2 := Hzu). split. apply Rle_trans with (xl * y)%R. exact (monotony_1p _ _ _ Hx Hyl). exact (monotony_2p _ _ _ (Rle_trans _ _ _ Hy Hyl) Hxl). apply Rle_trans with (x * yu)%R. exact (monotony_1p _ _ _ (Rle_trans _ _ _ Hx Hxl) Hyu). exact (monotony_2p _ _ _ (Rle_trans _ _ _ Hy (Rle_trans _ _ _ Hyl Hyu)) Hxu). Qed.
imports: Reals