brec_on and below

Stream: new members

[Sayantan Majumdar]

I was checking out the nat.below and nat.brec_on things and I was having some problems with a few proofs

def fib1 : ℕ → ℕ
| 0 := 1
| 1 := 1
| (n + 2) := fib1 (n + 1) + fib1 n

def fib2 : ℕ → ℕ :=
    assume n : ℕ,
    @nat.brec_on (λ n : ℕ, ℕ) n
    (
        assume n : ℕ,
        assume h : nat.below (λ n : ℕ, ℕ) n,
        (
            λ (n : ℕ) (h : nat.below (λ n : ℕ, ℕ) n),
            (@nat.cases_on (λ n : ℕ, nat.below (λ n : ℕ, ℕ) n → ℕ) n
            (λ h : nat.below (λ n : ℕ, ℕ) 0, 1)
            (
                assume n : ℕ,
                assume h : nat.below (λ n : ℕ, ℕ) (nat.succ n),
                (@nat.cases_on (λ n : ℕ, nat.below (λ n : ℕ, ℕ) (nat.succ n) → ℕ) n
                (λ h : nat.below (λ n : ℕ, ℕ) 1, 1)
                (
                    assume n : ℕ,
                    assume h : nat.below (λ n : ℕ, ℕ) (nat.succ (nat.succ n)),
                    (h.fst.fst + h.fst.snd.fst.fst)
                )) h
            )) h
        ) n h
    )

#reduce fib1 0
#reduce fib1 1
#reduce fib1 2
#reduce fib1 3
#reduce fib1 4
#reduce fib1 5
#reduce fib1 7

#reduce fib2 0
#reduce fib2 1
#reduce fib2 2
#reduce fib2 3
#reduce fib2 4
#reduce fib2 5
#reduce fib2 7

example : ∀ n : ℕ, fib1 n = fib2 n
| 0 := rfl
| 1 := rfl
| (n + 2) := sorry

[Sayantan Majumdar]

the (n + 2) := sorry part