theorem proved term proof

`minimal_coefficients`

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

formal statement (Lean)

  69theorem minimal_coefficients :
  70    ∀ a b : ℕ, 1 ≤ a → 1 ≤ b → 2 ≤ a + b :=

Term-mode proof.

  71  fun _ _ ha hb => by omega
  72
  73/-- (1,1) achieves the minimum. -/