calc
  m = fib k := hm
  _ ≤ fib K := fib_mono h3
case pos.left
N K : ℕ
HK : N < K.fib + (K + 1).fib
m n : ℕ
h1 : NatPredicate N m n
k : ℕ
hm : m = k.fib
hn : n = (k + 1).fib
h2 : k < K + 1
h3 : k ≤ K
⊢ m ≤ K.fib
no goals