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