Theorem: Imo1981P3.solution_greatest (Compfiles/Imo1981P3.lean)

State before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
H : ProblemPredicate N ↑K.fib ↑(K + 1).fib
⊢ ↑M = ↑K.fib ^ 2 + ↑(K + 1).fib ^ 2
Tactic:
simp [HM]
State after:
no goals