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

State before:
⊢ 4 ≠ 0
Tactic:
decide
State after:
no goals

State before:
⊢ 0 < 4
Tactic:
decide
State after:
no goals