proposition: Theorem IRminus : forall xl xu yl yu zl zu : R, (zl <= xl - yu)%R -> (xu - yl <= zu)%R -> forall x y : R, (xl <= x <= xu)%R -> (yl <= y <= yu)%R -> (zl <= x - y <= zu)%R.
proof: Proof. unfold Rminus. intros xl xu yl yu zl zu Hzl Hzu x y Hx Hy. apply IRplus with (1 := Hzl) (2 := Hzu) (3 := Hx). apply IRopp with (3 := Hy) ; auto with real. Qed.
imports: Reals