proposition: Lemma open_ball_half_radius_included X d r s x0 x1 : @metric X d -> In (open_ball d x1 s) x0 -> 0 < s < r / 2 -> Included (open_ball d x1 s) (open_ball d x0 r).
proof: Proof. intros ? ? ? z Hz. constructor. destruct Hz. destruct H0. apply (Rle_lt_trans _ (d x0 x1 + d x1 z)). { now apply triangle_inequality. } rewrite (metric_sym _ _ H x0 x1). lra. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)