n : ℕ
⊢ (if true = true then
      ((binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst ^
            2,
        (binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
              n).snd *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                    else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                  n).fst +
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd))
    else
      ((binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
              n).fst *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                    else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                  n).snd -
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst),
        (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst ^
            2)) =
    let p :=
      binaryRec (fib 0, fib 1)
        (fun b x p =>
          if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
          else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
        n;
    (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))

case h
n : ℕ
⊢ (if false = true then
      ((fib 0, fib 1).snd ^ 2 + (fib 0, fib 1).fst ^ 2,
        (fib 0, fib 1).snd * (2 * (fib 0, fib 1).fst + (fib 0, fib 1).snd))
    else
      ((fib 0, fib 1).fst * (2 * (fib 0, fib 1).snd - (fib 0, fib 1).fst),
        (fib 0, fib 1).snd ^ 2 + (fib 0, fib 1).fst ^ 2)) =
    (fib 0, fib 1)
n : ℕ
⊢ fastFibAux (bit true n) =
    let p := fastFibAux n;
    (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
rw [fastFibAux, binaryRec_eq]
no goals
n : ℕ
⊢ (if true = true then
      ((binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst ^
            2,
        (binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
              n).snd *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                    else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                  n).fst +
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd))
    else
      ((binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
              n).fst *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                    else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                  n).snd -
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst),
        (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst ^
            2)) =
    let p :=
      binaryRec (fib 0, fib 1)
        (fun b x p =>
          if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
          else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
        n;
    (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
rfl
no goals
case h
n : ℕ
⊢ (if false = true then
      ((fib 0, fib 1).snd ^ 2 + (fib 0, fib 1).fst ^ 2,
        (fib 0, fib 1).snd * (2 * (fib 0, fib 1).fst + (fib 0, fib 1).snd))
    else
      ((fib 0, fib 1).fst * (2 * (fib 0, fib 1).snd - (fib 0, fib 1).fst),
        (fib 0, fib 1).snd ^ 2 + (fib 0, fib 1).fst ^ 2)) =
    (fib 0, fib 1)
simp