P12 Coordination bottleneck

Declarations: P12_coordination_bottleneck

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P12_coordination_bottleneck
    {raw eff loss : Int}
    (hdef : eff = raw - loss) (hloss : 0 < loss) :
    eff < raw := by omega