proposition: Lemma IRdiv_aux_n : forall yl yu y : R, (yu < 0)%R -> (yl <= y <= yu)%R -> (/ yl <= 0)%R /\ (/ yu <= 0)%R /\ (yl <> 0)%R /\ (yu <> 0)%R /\ (/ yu <= /y <= / yl)%R.
proof: Proof. intros yl yu y Hyu Hy. split. left. apply Rinv_lt_0_compat. exact (Rle_lt_trans _ _ _ (Rle_trans _ _ _ (proj1 Hy) (proj2 Hy)) Hyu). split. left. apply Rinv_lt_0_compat. exact Hyu. split. apply Rlt_not_eq. exact (Rle_lt_trans _ _ _ (Rle_trans _ _ _ (proj1 Hy) (proj2 Hy)) Hyu). split. apply Rlt_not_eq. exact Hyu. split. exact (Rle_Rinv_neg _ _ Hyu (proj2 Hy)). exact (Rle_Rinv_neg _ _ (Rle_lt_trans _ _ _ (proj2 Hy) Hyu) (proj1 Hy)). Qed.
imports: Reals