proposition: Lemma disc_P1 : forall (x:R) (del:posreal), open_set (disc x del).
proof: Proof. intros; assert (H := open_set_P1 (disc x del)). elim H; intros; apply H1. unfold eq_Dom; split. - unfold included, interior, disc; intros; cut (0 < del - Rabs (x - x0)). + intro; set (del2 := mkposreal _ H3). exists del2; unfold included; intros. apply Rle_lt_trans with (Rabs (x1 - x0) + Rabs (x0 - x)). * replace (x1 - x) with (x1 - x0 + (x0 - x)); [ apply Rabs_triang | ring ]. * replace (pos del) with (del2 + Rabs (x0 - x)). -- do 2 rewrite <- (Rplus_comm (Rabs (x0 - x))); apply Rplus_lt_compat_l. apply H4. -- unfold del2; simpl; rewrite <- (Rabs_Ropp (x - x0)); rewrite Ropp_minus_distr; ring. + apply Rplus_lt_reg_l with (Rabs (x - x0)); rewrite Rplus_0_r; replace (Rabs (x - x0) + (del - Rabs (x - x0))) with (pos del); [ rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H2 | ring ]. - apply interior_P1. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type