case zero
n : ℕ
a b f g : Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : Vector ℕ n
e : b v - a v = Nat.zero
⊢ Nat.rec (g v) (fun y IH => f (Vector.tail (Vector.tail (y ::ᵥ IH ::ᵥ v)))) Nat.zero = if a v < b v then f v else g v

case succ
n : ℕ
a b f g : Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : Vector ℕ n
n✝ : ℕ
e : b v - a v = Nat.succ n✝
⊢ Nat.rec (g v) (fun y IH => f (Vector.tail (Vector.tail (y ::ᵥ IH ::ᵥ v)))) (Nat.succ n✝) =
    if a v < b v then f v else g v
n : ℕ
a b f g : Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : Vector ℕ n
⊢ Nat.rec (g v) (fun y IH => f (Vector.tail (Vector.tail (y ::ᵥ IH ::ᵥ v)))) (b v - a v) =
    if a v < b v then f v else g v
cases e : b v - a v
no goals
case zero
n : ℕ
a b f g : Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : Vector ℕ n
e : b v - a v = Nat.zero
⊢ Nat.rec (g v) (fun y IH => f (Vector.tail (Vector.tail (y ::ᵥ IH ::ᵥ v)))) Nat.zero = if a v < b v then f v else g v
simp [not_lt.2 (tsub_eq_zero_iff_le.mp e)]
no goals
case succ
n : ℕ
a b f g : Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : Vector ℕ n
n✝ : ℕ
e : b v - a v = Nat.succ n✝
⊢ Nat.rec (g v) (fun y IH => f (Vector.tail (Vector.tail (y ::ᵥ IH ::ᵥ v)))) (Nat.succ n✝) =
    if a v < b v then f v else g v
simp [Nat.lt_of_sub_eq_succ e]