theorem norm_symm (x y : ℤ) : ‖![x, y]‖ = ‖![y, x]‖

theorem linear_bigO (m : ℤ) (z : UpperHalfPlane) : (fun (n : ℤ) => (↑m * ↑z + ↑n)⁻¹) =O[Filter.cofinite] fun (n : ℤ) => |↑n|⁻¹

theorem linear_bigO_pow (m : ℤ) (z : UpperHalfPlane) (k : ℕ) : (fun (n : ℤ) => ((↑m * ↑z + ↑n) ^ k)⁻¹) =O[Filter.cofinite] fun (n : ℤ) => (|↑n| ^ k)⁻¹

theorem Asymptotics.IsBigO.zify {α : Type u_1} {β : Type u_2} [Norm α] [Norm β] {f : ℤ → α} {g : ℤ → β} (hf : f =O[Filter.cofinite] g) : (fun (n : ℕ) => f ↑n) =O[Filter.cofinite] fun (n : ℕ) => g ↑n

theorem Asymptotics.IsBigO.of_neg {α : Type u_1} {β : Type u_2} [Norm α] [Norm β] {f : ℤ → α} {g : ℤ → β} (hf : f =O[Filter.cofinite] g) : (fun (n : ℤ) => f (-n)) =O[Filter.cofinite] fun (n : ℤ) => g (-n)

theorem linear_bigO_nat (m : ℤ) (z : UpperHalfPlane) : (fun (n : ℕ) => (↑m * ↑z + ↑n)⁻¹) =O[Filter.cofinite] fun (n : ℕ) => |↑n|⁻¹

theorem linear_bigO' (m : ℤ) (z : UpperHalfPlane) : (fun (n : ℤ) => (↑n * ↑z + ↑m)⁻¹) =O[Filter.cofinite] fun (n : ℤ) => |↑n|⁻¹