List.Chain forward induction

Stream: mathlib4

[Daniel Weber]

Currently docs#List.Chain.induction is stated from the end of the chain, and induction from the start of the chain seems to be missing. Does it exist somewhere that I missed?

[Daniel Weber]

If not, I want to add

theorem Chain.induction (p : α → Prop) (l : List α) (h : Chain r a l)
    (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) : ∀ i ∈ l, p i

and rename the current Chain.induction to Chain.backwards_induction