proposition: Theorem IRopp : forall yl yu zl zu : R, (zl <= -yu)%R -> (-yl <= 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). apply IRsubset with (1 := Hzl) (2 := Hzu). split. apply Ropp_le_contravar with (1 := Hyu). apply Ropp_le_contravar with (1 := Hyl). Qed.
imports: Reals