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