proposition: Lemma Rbar_lt_locally (a b : Rbar) (x : R) : Rbar_lt a x -> Rbar_lt x b -> exists delta : posreal, forall y, Rabs (y - x) < delta -> Rbar_lt a y /\ Rbar_lt y b.
proof: Proof. case: a => [ a /= Ha | | _ ] //= ; (try apply Rminus_lt_0 in Ha) ; case: b => [ b Hb | _ | ] //= ; (try apply Rminus_lt_0 in Hb). assert (0 < Rmin (x - a) (b - x)). by apply Rmin_case. exists (mkposreal _ H) => y /= Hy ; split. apply Rplus_lt_reg_r with (-x). replace (a+-x) with (-(x-a)) by ring. apply (Rabs_lt_between (y - x)). apply Rlt_le_trans with (1 := Hy). by apply Rmin_l. apply Rplus_lt_reg_r with (-x). apply (Rabs_lt_between (y - x)). apply Rlt_le_trans with (1 := Hy). by apply Rmin_r. exists (mkposreal _ Ha) => y /= Hy ; split => //. apply Rplus_lt_reg_r with (-x). replace (a+-x) with (-(x-a)) by ring. by apply (Rabs_lt_between (y - x)). exists (mkposreal _ Hb) => y /= Hy ; split => //. apply Rplus_lt_reg_r with (-x). by apply (Rabs_lt_between (y - x)). exists (mkposreal _ Rlt_0_1) ; by split. Qed.
imports: Coq(Reals ssreflect) Rcomplements