proposition: Theorem IRabs_p : forall yl yu zl zu : R, (0 <= yl)%R -> (zl <= yl)%R -> (yu <= 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_pos_eq. apply IRsubset with (1 := Hzl) (2 := Hzu) (3 := Hylu). apply Rle_trans with (1 := Hy) (2 := proj1 Hylu). Qed.
imports: Reals