Theorem: Imo1969P1.aChoice_good (Compfiles/Imo1969P1.lean)

State before:
b : ℕ
⊢ 1 < 2 + b
Tactic:
omega
State after:
no goals