theorem proved term proof

`unit_coefficients_minimal`

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

formal statement (Lean)

  74theorem unit_coefficients_minimal :
  75    ∀ a b : ℕ, 1 ≤ a → 1 ≤ b → 1 + 1 ≤ a + b :=

Term-mode proof.

  76  fun _ _ ha hb => by omega
  77
  78/-! ## The Derivation: Z_ℓ = 1332 -/
  79
  80/-- Z_poly with (a,b) = (1,1) at Q̃ = -6 gives 1332. -/

Lean names referenced from this declaration's body.