apply ind_on (motive := λ x => x * (m + k) ≃ x * m + x * k) n
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ n * (m + k) ≃ n * m + n * k
case zero
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ 0 * (m + k) ≃ 0 * m + 0 * k

case step
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ ∀ (m_1 : ℕ), m_1 * (m + k) ≃ m_1 * m + m_1 * k → step m_1 * (m + k) ≃ step m_1 * m + step m_1 * k