apply lt_mul_of_one_lt_right (Int.natAbs_pos.mpr (mul_ne_zero two_ne_zero hp))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ Int.natAbs (2 * p) < Int.natAbs (2 * p) * Int.natAbs (Zsqrtd.norm P)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ 1 < Int.natAbs (Zsqrtd.norm P)