K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
⊢ Stream'.Seq.get? (of ↑a).s n = none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ ∀ (n : ℕ), Stream'.Seq.get? (of ↑a).s n = none
intro n
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ Stream'.Seq.get? (of ↑a).s Nat.zero = none

case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
ih : Stream'.Seq.get? (of ↑a).s n = none
⊢ Stream'.Seq.get? (of ↑a).s (Nat.succ n) = none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
⊢ Stream'.Seq.get? (of ↑a).s n = none
induction' n with n ih
no goals
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ Stream'.Seq.get? (of ↑a).s Nat.zero = none
rw [of_s_head_aux, stream_succ_of_int, Option.bind]
no goals
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
ih : Stream'.Seq.get? (of ↑a).s n = none
⊢ Stream'.Seq.get? (of ↑a).s (Nat.succ n) = none
exact (of (a : K)).s.prop ih