ι : Type ?u.238764
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b : β
a✝ : α
l✝ : List α
a : β
x : α
l : List α
⊢ length (scanl f (f a x) l) = length l + 1
ι : Type ?u.238764
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b : β
a✝ : α
l✝ : List α
a : β
x : α
l : List α
⊢ length (scanl f a (x :: l)) = length (x :: l) + 1
rw [scanl, length_cons, length_cons, ←succ_eq_add_one, congr_arg succ]
no goals
ι : Type ?u.238764
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b : β
a✝ : α
l✝ : List α
a : β
x : α
l : List α
⊢ length (scanl f (f a x) l) = length l + 1
exact length_scanl _ _