α : Type ?u.316248
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
a : ℤ
⊢ ↑(natAbs a) ≤ ↑(natAbs a) * ↑(natAbs a)
α : Type ?u.316248
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
a : ℤ
⊢ ↑(natAbs a) ≤ a ^ 2
rw [← Int.natAbs_sq a, sq]
α : Type ?u.316248
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
a : ℤ
⊢ natAbs a ≤ natAbs a * natAbs a
α : Type ?u.316248
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
a : ℤ
⊢ ↑(natAbs a) ≤ ↑(natAbs a) * ↑(natAbs a)
norm_cast
no goals
α : Type ?u.316248
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
a : ℤ
⊢ natAbs a ≤ natAbs a * natAbs a
apply Nat.le_mul_self