a b n : ℕ
h : a * b = n
h₁ : 1 < a
h₂ : 1 < b
⊢ ¬Prime (a * b)
a b n : ℕ
h : a * b = n
h₁ : 1 < a
h₂ : 1 < b
⊢ ¬Prime n
rw [← h]
no goals
a b n : ℕ
h : a * b = n
h₁ : 1 < a
h₂ : 1 < b
⊢ ¬Prime (a * b)
exact not_prime_mul h₁ h₂