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

State before:
m : ℤ
h : 1 < m
⊢ 1 < m.natAbs
Tactic:
exact_mod_cast lt_of_lt_of_le h le_natAbs
State after:
no goals