proposition: Lemma every_point_in_R_acc_point_R (a : R) : is_accumulation_point a.
proof: Proof. We need to show that (∀ r : R, r > 0 ⇒ ∃ x : R, 0 < | x - a | < r). Take r : R. Assume that (r > 0). Choose x := (a + r/2). It holds that (| x - a | < r). It holds that (| x - a | > 0). We conclude that (0 < | x - a | < r). Qed.
imports: Coq.Reals.Reals Notations Tactics Waterproof.Automation