cases' n with n
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
n : ℕ
hn : 0 < n
⊢ is_decent (Stream'.take n a)
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
hn : 0 < 0
⊢ is_decent (Stream'.take 0 a)

case succ
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
n : ℕ
hn : 0 < n + 1
⊢ is_decent (Stream'.take (n + 1) a)