exact absurd h7 h9.not_lt
case neg
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
h7 : N < n
h9 : n ≤ N
⊢ m ≤ K.fib ∧ n ≤ (K + 1).fib
no goals