obtain ⟨k : ℕ, hnm : n - m = fib k, rfl : m = fib (k + 1)⟩ := h1 m h6 (n - m) h7
case inr.inr
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
m : ℕ
h2 : NatPredicate N m n
h3 : m ≤ n
h4 : 1 < n
h6 : m < n
h7 : NatPredicate N (n - m) m
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib
case inr.inr.intro.intro
N n✝ n : ℕ
h1 : ∀ m < n, ∀ (m_1 : ℕ), NatPredicate N m_1 m → ∃ k, m_1 = k.fib ∧ m = (k + 1).fib
h4 : 1 < n
k : ℕ
h2 : NatPredicate N (k + 1).fib n
h3 : (k + 1).fib ≤ n
h6 : (k + 1).fib < n
h7 : NatPredicate N (n - (k + 1).fib) (k + 1).fib
hnm : n - (k + 1).fib = k.fib
⊢ ∃ k_1, (k + 1).fib = k_1.fib ∧ n = (k_1 + 1).fib