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

State before:
m n : ℤ
h : 1 < m
⊢ 1 < (n - m) ^ 2 + m ^ 2
Tactic:
nlinarith
State after:
no goals