have : Positive n := positive_defn.mpr ‹n ≄ 0›
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
this✝ : n * m ≄ 0
this : ¬(n ≃ 0 ∨ m ≃ 0)
left✝ : n ≄ 0
right✝ : m ≄ 0
⊢ Positive n ∧ Positive m
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
this✝¹ : n * m ≄ 0
this✝ : ¬(n ≃ 0 ∨ m ≃ 0)
left✝ : n ≄ 0
right✝ : m ≄ 0
this : Positive n
⊢ Positive n ∧ Positive m