A product divided by its consecutive sum
ProvedWorkbookSource.problem_35661lean-workbooksource-checked
The quotient of the product of the first eight positive integers by their sum is
The numerator is divisible by the denominator, so the source natural-number quotient agrees with ordinary division.
Source: InternLM Lean-Workbook, record lean_workbook_35661 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_35661 (h : 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 ≠ 0) : 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 / (1 + 2 + 3 + 4 + 5 + 6 + 7 + 8) = 1120 := by sorry
Source