case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ max (stationaryPoint hf) (max v2 v3)

case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max (stationaryPoint hf) (max v2 v3)))
apply stationaryPoint_spec hf
no goals
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ max (stationaryPoint hf) (max v2 v3)
apply le_max_left
no goals
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf
exact le_rfl