proposition: Lemma IRinv_disj : forall yl yu zl zu : R, (yu < 0)%R \/ (0 < yl)%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 [Hy2|Hy1] Hzl Hzu y Hy. exact (IRinv_n _ _ _ _ Hy2 Hzl Hzu _ Hy). exact (IRinv_p _ _ _ _ Hy1 Hzl Hzu _ Hy). Qed.
imports: Reals