Theorem: Imo1981P3.ProblemPredicate.eq_imp_1 (Compfiles/Imo1981P3.lean)

State before:
N : ℕ
n : ℤ
h1 : ProblemPredicate N n n
⊢ n * (n * (n * n)) = 1
Tactic:
linear_combination h1.eq_one
State after:
no goals