proposition: Theorem IRsubset : forall yl yu zl zu : R, (zl <= yl)%R -> (yu <= zu)%R -> forall y : R, (yl <= y <= yu)%R -> (zl <= y <= zu)%R.
proof: Proof. intros yl yu zl zu Hzl Hzu y (Hyl,Hyu). split. apply Rle_trans with (1 := Hzl) (2 := Hyl). apply Rle_trans with (1 := Hyu) (2 := Hzu). Qed.
imports: Reals