no goals
𝕜 : Type u_1
B : Type ?u.42067
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p x : 𝕜
⊢ ↑(x + p) = ↑x
rw [coe_add, ← eq_sub_iff_add_eq', sub_self, coe_period]