obtain (rfl : m = n) | (h6 : m < n) := h3.eq_or_lt
case 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
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib
case inr.inl
N n m : ℕ
h1 : ∀ m_1 < m, ∀ (m : ℕ), NatPredicate N m m_1 → ∃ k, m = k.fib ∧ m_1 = (k + 1).fib
h2 : NatPredicate N m m
h3 : m ≤ m
h4 : 1 < m
⊢ ∃ k, m = k.fib ∧ m = (k + 1).fib

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
⊢ ∃ k, m = k.fib ∧ n = (k + 1).fib