proposition: Theorem IRmult_oo : forall xl xu yl yu zl zu : R, (xl <= 0)%R -> (0 <= xu)%R -> (yl <= 0)%R -> (0 <= yu)%R -> (zl <= xu * yl)%R -> (zl <= xl * yu)%R -> (xl * yl <= zu)%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 Hx1 Hx2 Hy1 Hy2 Hzl1 Hzl2 Hzu1 Hzu2 x y (Hxl,Hxu) (Hyl,Hyu). case (Rlt_le_dec 0 x) ; intro H. generalize (Rlt_le _ _ H). clear H. intro H. split. apply Rle_trans with (1 := Hzl1). apply Rle_trans with (x * yl)%R. exact (monotony_2n _ _ _ Hy1 Hxu). exact (monotony_1p _ _ _ H Hyl). apply Rle_trans with (2 := Hzu2). apply Rle_trans with (x * yu)%R. exact (monotony_1p _ _ _ H Hyu). exact (monotony_2p _ _ _ Hy2 Hxu). split. apply Rle_trans with (1 := Hzl2). apply Rle_trans with (x * yu)%R. exact (monotony_2p _ _ _ Hy2 Hxl). exact (monotony_1n _ _ _ H Hyu). apply Rle_trans with (2 := Hzu1). apply Rle_trans with (x * yl)%R. exact (monotony_1n _ _ _ H Hyl). exact (monotony_2n _ _ _ Hy1 Hxl). Qed.
imports: Reals