theorem proved term proof

`only_11_6_sum_to_17`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  76theorem only_11_6_sum_to_17 :
  77    (13 + 11 ≠ 17) ∧ (13 + 6 ≠ 17) ∧ (13 + 8 ≠ 17) ∧
  78    (11 + 8 ≠ 17) ∧ (6 + 8 ≠ 17) ∧
  79    (11 + 6 = 17) := by

proof body

Term-mode proof.

  80  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;> omega
  81
  82/-- The middle pair {b, c} must be {11, 6} (in either order). -/