no goals
F : Type ?u.197857
α : Type ?u.197860
β : Type ?u.197863
𝕜 : Type ?u.197866
E : Type ?u.197869
s : Finset ℕ
k n : ℕ
⊢ ∀ (x : ℕ), ‖↑(↑rothNumberNat x)‖ ≤ ‖↑x‖
simpa only [Real.norm_coe_nat, Nat.cast_le] using rothNumberNat_le