A difference of two cubes
ProvedWorkbookSource.problem_5606lean-workbooksource-checked
Find the value of given , , and
Source: InternLM Lean-Workbook, record lean_workbook_5606 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_5606 (a b n : ℕ) (hab : a = 4 ∧ b = 2) (hn : n = 3) : a^n - b^n = 56 := by sorry
Source