proposition: Theorem IRabs_o : forall yl yu zl zu : R, (zl <= 0)%R -> (-yl <= zu)%R -> (yu <= zu)%R -> forall y : R, (yl <= y <= yu)%R -> (zl <= Rabs y <= zu)%R.
proof: Proof. intros yl yu zl zu Hzl Hzu1 Hzu2 y (Hyl,Hyu). split. apply Rle_trans with (1 := Hzl) (2 := Rabs_pos y). unfold Rabs. case Rcase_abs ; intro H. apply Rle_trans with (2 := Hzu1). apply Ropp_le_contravar with (1 := Hyl). apply Rle_trans with (1 := Hyu) (2 := Hzu2). Qed.
imports: Reals