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