proposition: Theorem IRdiv_op : forall xl xu yl yu zl zu : R, (xl <= 0)%R -> (0 <= xu)%R -> (0 < yl)%R -> (yl * zl <= xl)%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 Hxl Hxu Hyl Hzl Hzu x y Hx Hy. generalize (IRdiv_aux_p _ _ _ Hyl Hy). intros (Hy1, (Hy2, (Hy3, (Hy4, Hy5)))). unfold Rdiv. apply IRmult_op with (1 := Hxl) (2 := Hxu) (3 := Hy2) (6 := Hx) (7 := Hy5). replace zl with (yl * zl * / yl)%R. exact (monotony_2p _ _ _ Hy1 Hzl). field. exact Hy3. replace zu with (yl * zu * / yl)%R. exact (monotony_2p _ _ _ Hy1 Hzu). field. exact Hy3. Qed.
imports: Reals