proposition: Theorem IRabs_n : forall yl yu zl zu : R, (yu <= 0)%R -> (zl <= -yu)%R -> (-yl <= zu)%R -> forall y : R, (yl <= y <= yu)%R -> (zl <= Rabs y <= zu)%R.
proof: Proof. intros yl yu zl zu Hy Hzl Hzu y Hylu. rewrite Rabs_left1. apply IRopp with (1 := Hzl) (2 := Hzu) (3 := Hylu). apply Rle_trans with (1 := proj2 Hylu) (2 := Hy). Qed.
imports: Reals