proposition: Lemma IRmult_minmax : forall xl xu yl yu zl zu : R, (zl <= Rmin (Rmin (xl * yl) (xl * yu)) (Rmin (xu * yl) (xu * yu)))%R -> (Rmax (Rmax (xl * yl) (xl * yu)) (Rmax (xu * yl) (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 Hzl Hzu x y Hx Hy. decompose [and] (Rmin_trans _ _ _ Hzl). decompose [and] (Rmin_trans _ _ _ H). decompose [and] (Rmin_trans _ _ _ H0). clear Hzl H H0. decompose [and] (Rmax_trans _ _ _ Hzu). decompose [and] (Rmax_trans _ _ _ H). decompose [and] (Rmax_trans _ _ _ H0). clear Hzu H H0. case (interval_sign_correct _ _ (Rle_trans _ _ _ (proj1 Hx) (proj2 Hx))) ; case (interval_sign_correct _ _ (Rle_trans _ _ _ (proj1 Hy) (proj2 Hy))) ; intros. apply IRmult_nn with xl xu yl yu ; assumption. apply IRmult_no with xl xu yl yu ; assumption. apply IRmult_np with xl xu yl yu ; assumption. apply IRmult_on with xl xu yl yu ; assumption. apply IRmult_oo with xl xu yl yu ; assumption. apply IRmult_op with xl xu yl yu ; assumption. apply IRmult_pn with xl xu yl yu ; assumption. apply IRmult_po with xl xu yl yu ; assumption. apply IRmult_pp with xl xu yl yu ; assumption. Qed.
imports: Reals