n : ℕ
x : ℕ × ℕ
h : x.fst * x.snd = n ∧ n ≠ 0
⊢ x.fst ∈ divisors n
n : ℕ
x : ℕ × ℕ
h : x ∈ divisorsAntidiagonal n
⊢ x.fst ∈ divisors n
rw [mem_divisorsAntidiagonal] at h
no goals
n : ℕ
x : ℕ × ℕ
h : x.fst * x.snd = n ∧ n ≠ 0
⊢ x.fst ∈ divisors n
simp [Dvd.intro _ h.1, h.2]