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