case mk
α : Type u
β : Type v
γ : Type w
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : IsSeq f
⊢ get? { val := f, property := al } m = none → get? { val := f, property := al } n = none
α : Type u
β : Type v
γ : Type w
s : Seq α
m n : ℕ
h : m ≤ n
⊢ get? s m = none → get? s n = none
cases' s with f al
case mk.refl
α : Type u
β : Type v
γ : Type w
m n : ℕ
f : Stream' (Option α)
al : IsSeq f
⊢ get? { val := f, property := al } m = none → get? { val := f, property := al } m = none

case mk.step
α : Type u
β : Type v
γ : Type w
m n✝ : ℕ
f : Stream' (Option α)
al : IsSeq f
n : ℕ
a✝ : Nat.le m n
IH : get? { val := f, property := al } m = none → get? { val := f, property := al } n = none
⊢ get? { val := f, property := al } m = none → get? { val := f, property := al } (Nat.succ n) = none
case mk
α : Type u
β : Type v
γ : Type w
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : IsSeq f
⊢ get? { val := f, property := al } m = none → get? { val := f, property := al } n = none
induction' h with n _ IH
no goals
case mk.refl
α : Type u
β : Type v
γ : Type w
m n : ℕ
f : Stream' (Option α)
al : IsSeq f
⊢ get? { val := f, property := al } m = none → get? { val := f, property := al } m = none

case mk.step
α : Type u
β : Type v
γ : Type w
m n✝ : ℕ
f : Stream' (Option α)
al : IsSeq f
n : ℕ
a✝ : Nat.le m n
IH : get? { val := f, property := al } m = none → get? { val := f, property := al } n = none
⊢ get? { val := f, property := al } m = none → get? { val := f, property := al } (Nat.succ n) = none
exacts [id, fun h2 => al (IH h2)]