constructor
case pos
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 ∧ n ≤ (K + 1).fib
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

case pos.right
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
⊢ n ≤ (K + 1).fib