no goals
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico 0 p
⊢ x ∈ Ico 0 (0 + p)
rwa [zero_add]