[GOAL]
⊢ DecidableRel fun x x_1 => x ≤ x_1
[PROOFSTEP]
infer_instance
[GOAL]
⊢ DecidableEq ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ DecidableRel fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
a b : ℤ
h : a * b = 0
hlt₁ : 0 < a
hlt₂ : 0 < b
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
have : 0 < a * b := Int.mul_pos hlt₁ hlt₂
[GOAL]
a b : ℤ
h : a * b = 0
hlt₁ : 0 < a
hlt₂ : 0 < b
this : 0 < a * b
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
rw [h] at this 
[GOAL]
a b : ℤ
h : a * b = 0
hlt₁ : 0 < a
hlt₂ : 0 < b
this : 0 < 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
exact absurd this (lt_irrefl _)
[GOAL]
a b : ℤ
h : a * b = 0
hlt₁ : 0 < a
hgt₂ : b < 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
have : 0 > a * b := Int.mul_neg_of_pos_of_neg hlt₁ hgt₂
[GOAL]
a b : ℤ
h : a * b = 0
hlt₁ : 0 < a
hgt₂ : b < 0
this : 0 > a * b
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
rw [h] at this 
[GOAL]
a b : ℤ
h : a * b = 0
hlt₁ : 0 < a
hgt₂ : b < 0
this : 0 > 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
exact absurd this (lt_irrefl _)
[GOAL]
a b : ℤ
h : a * b = 0
hgt₁ : a < 0
hlt₂ : 0 < b
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
have : 0 > a * b := Int.mul_neg_of_neg_of_pos hgt₁ hlt₂
[GOAL]
a b : ℤ
h : a * b = 0
hgt₁ : a < 0
hlt₂ : 0 < b
this : 0 > a * b
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
rw [h] at this 
[GOAL]
a b : ℤ
h : a * b = 0
hgt₁ : a < 0
hlt₂ : 0 < b
this : 0 > 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
exact absurd this (lt_irrefl _)
[GOAL]
a b : ℤ
h : a * b = 0
hgt₁ : a < 0
hgt₂ : b < 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
have : 0 < a * b := Int.mul_pos_of_neg_of_neg hgt₁ hgt₂
[GOAL]
a b : ℤ
h : a * b = 0
hgt₁ : a < 0
hgt₂ : b < 0
this : 0 < a * b
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
rw [h] at this 
[GOAL]
a b : ℤ
h : a * b = 0
hgt₁ : a < 0
hgt₂ : b < 0
this : 0 < 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
exact absurd this (lt_irrefl _)
