theorem proved term proof

`additive_composition_is_minimal`

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

formal statement (Lean)

 108theorem additive_composition_is_minimal (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b) :
 109    max a b = 1 → a = 1 ∧ b = 1 := by

proof body

Term-mode proof.

 110  intro h
 111  constructor
 112  · exact Nat.le_antisymm (by omega) ha
 113  · exact Nat.le_antisymm (by omega) hb
 114
 115/-- The pair (1,1) achieves max = 1. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

zero_param_forces_unit_coefficients in IndisputableMonolith.Foundation.HierarchyDynamics decl_use

depends on (1)

Lean names referenced from this declaration's body.

le_antisymm in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use