proposition: Lemma IRinv_n : forall yl yu zl zu, (yu < 0)%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 Hy Hzl Hzu y (Hyl,Hyu). apply IRsubset with (1 := Hzl) (2 := Hzu). split. exact (Rle_Rinv_neg _ _ Hy Hyu). apply Rle_Rinv_neg with (2 := Hyl). exact (Rle_lt_trans _ _ _ Hyu Hy). Qed.
imports: Reals