proposition: Lemma IRdiv_minmax : forall xl xu yl yu zl zu : R, (yu < 0)%R \/ (yl > 0)%R -> (zl <= Rmin (Rmin (xl / yu) (xl / yl)) (Rmin (xu / yu) (xu / yl)))%R -> (Rmax (Rmax (xl / yu) (xl / yl)) (Rmax (xu / yu) (xu / yl)) <= zu)%R -> forall x y : R, (xl <= x <= xu)%R -> (yl <= y <= yu)%R -> (zl <= x / y <= zu)%R.
proof: Proof. unfold Rdiv. intros xl xu yl yu zl zu H Hzl Hzu x y Hx Hy. apply (IRmult_minmax _ _ (/yu) (/yl) _ _ Hzl Hzu _ (/y) Hx). apply (IRinv_disj _ _ (/yu) (/yl) H) with (3 := Hy) ; auto with real. Qed.
imports: Reals