case ofNat
𝕜 : Type u_1
B : Type ?u.190115
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : Nat.gcd (Int.natAbs (Int.ofNat a✝)) n = 1
⊢ addOrderOf ↑(↑(Int.ofNat a✝) / ↑n * p) = n

case negSucc
𝕜 : Type u_1
B : Type ?u.190115
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : Nat.gcd (Int.natAbs (Int.negSucc a✝)) n = 1
⊢ addOrderOf ↑(↑(Int.negSucc a✝) / ↑n * p) = n
𝕜 : Type u_1
B : Type ?u.190115
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
m : ℤ
n : ℕ
hn : 0 < n
h : Nat.gcd (Int.natAbs m) n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n
induction m
case ofNat
𝕜 : Type u_1
B : Type ?u.190115
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : Nat.gcd a✝ n = 1
⊢ addOrderOf ↑(↑a✝ / ↑n * p) = n
case ofNat
𝕜 : Type u_1
B : Type ?u.190115
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : Nat.gcd (Int.natAbs (Int.ofNat a✝)) n = 1
⊢ addOrderOf ↑(↑(Int.ofNat a✝) / ↑n * p) = n
simp only [Int.ofNat_eq_coe, Int.cast_ofNat, Int.natAbs_ofNat] at h⊢
no goals
case ofNat
𝕜 : Type u_1
B : Type ?u.190115
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : Nat.gcd a✝ n = 1
⊢ addOrderOf ↑(↑a✝ / ↑n * p) = n
exact addOrderOf_div_of_gcd_eq_one hn h
case negSucc
𝕜 : Type u_1
B : Type ?u.190115
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : Nat.gcd (Int.natAbs (Int.negSucc a✝)) n = 1
⊢ addOrderOf ↑(↑(a✝ + 1) / ↑n * p) = n
case negSucc
𝕜 : Type u_1
B : Type ?u.190115
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : Nat.gcd (Int.natAbs (Int.negSucc a✝)) n = 1
⊢ addOrderOf ↑(↑(Int.negSucc a✝) / ↑n * p) = n
simp only [Int.cast_negSucc, neg_div, neg_mul, coe_neg, addOrderOf_neg]
no goals
case negSucc
𝕜 : Type u_1
B : Type ?u.190115
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : Nat.gcd (Int.natAbs (Int.negSucc a✝)) n = 1
⊢ addOrderOf ↑(↑(a✝ + 1) / ↑n * p) = n
exact addOrderOf_div_of_gcd_eq_one hn h