proposition: Lemma locally_not' : forall (x : T) (P : T -> Prop), not (forall eps : posreal, not (forall y, ball x eps y -> not (P y))) -> {d : posreal | forall y, ball x d y -> not (P y)}.
proof: Proof. intros x P H. set (Q := fun z => z <= 1 /\ forall y, ball x z y -> not (P y)). destruct (completeness Q) as [d [H1 H2]]. - exists 1. now intros y [Hy _]. - exists 0. split. apply Rle_0_1. intros y Hy Py. apply H. intros eps He. apply He with (2 := Py). apply ball_le with (2 := Hy). apply Rlt_le, eps. assert (Zd : 0 < d). apply Rnot_le_lt. intros Hd. apply H. intros eps He. apply (Rlt_irrefl (Rmin 1 eps)). apply Rle_lt_trans with d. apply H1. split. apply Rmin_l. intros y By. apply He. apply ball_le with (2 := By). apply Rmin_r. apply Rle_lt_trans with (1 := Hd). apply Rmin_case. apply Rlt_0_1. apply cond_pos. exists (mkposreal _ (is_pos_div_2 (mkposreal _ Zd))). simpl. intros y Hy HP. apply (Rlt_not_le _ _ (Rlt_eps2_eps _ Zd)). apply H2. intros z Hz. apply Rnot_lt_le. contradict HP. apply Hz. apply ball_le with (2 := Hy). now apply Rlt_le. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub