clear h2 h3
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h2 : 0 ≤ m
h3 : 0 ≤ n
⊢ m ^ 2 + n ^ 2 ≤ ↑M
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
⊢ m ^ 2 + n ^ 2 ≤ ↑M