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