start induction with `m = 2`

Stream: Is there code for X?

[Asei Inoue]

import Mathlib.Tactic

variable (m n : ℕ)

/-- linear time implementation of the fibonacci sequence -/
def fib (n : Nat) : Nat :=
  (loop n).1
where
  loop : Nat → Nat × Nat
    | 0   => (0, 1)
    | n + 1 =>
      let p := loop n
      (p.2, p.1 + p.2)

/-- basic property of `fib` -/
theorem fib_add (n : Nat) : fib n + fib (n + 1) = fib (n + 2) := by rfl

@[simp]
lemma fib_zero : fib 0 = 0 := by rfl

lemma fib_cross_add (hm : 1 < m) (hn : m < n) : fib n = fib m * fib (n - m + 1) + fib (m - 1) * fib (n - m)  := by
  induction' m with k ih
  -- start with case `m = 0`
  -- I want to start induction with `m = 2`
  · contradiction
  · sorry

[Asei Inoue]

I want to start induction with case m = 2 using hypothesis hm.

[Asei Inoue]

Is there code for this?

[Ruben Van de Velde]

lemma fib_cross_add (hm : 1 < m) (hn : m < n) : fib n = fib m * fib (n - m + 1) + fib (m - 1) * fib (n - m)  := by
  rw [← Nat.succ_le_iff] at hm
  induction m, hm using Nat.le_induction with
  | base => sorry
  | succ k ih => sorry

[Asei Inoue]

@Ruben Van de Velde Thanks