proposition: Lemma IRdiv_aux_p : forall yl yu y : R, (0 < yl)%R -> (yl <= y <= yu)%R -> (0 <= / yl)%R /\ (0 <= / yu)%R /\ (yl <> 0)%R /\ (yu <> 0)%R /\ (/ yu <= /y <= / yl)%R.
proof: Proof. intros yl yu y Hyl Hy. split. left. apply Rinv_0_lt_compat. exact Hyl. split. left. apply Rinv_0_lt_compat. exact (Rlt_le_trans _ _ _ Hyl (Rle_trans _ _ _ (proj1 Hy) (proj2 Hy))). split. apply Rgt_not_eq. exact Hyl. split. apply Rgt_not_eq. exact (Rlt_le_trans _ _ _ Hyl (Rle_trans _ _ _ (proj1 Hy) (proj2 Hy))). split. exact (Rle_Rinv_pos _ _ (Rlt_le_trans _ _ _ Hyl (proj1 Hy)) (proj2 Hy)). exact (Rle_Rinv_pos _ _ Hyl (proj1 Hy)). Qed.
imports: Reals