case zero
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ FP (Stream'.drop Nat.zero a) ⊆ FP a

case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop (Nat.succ n) a) ⊆ FP a
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
⊢ FP (Stream'.drop n a) ⊆ FP a
induction' n with n ih
case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop 1 (Stream'.drop n a)) ⊆ FP a
case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop (Nat.succ n) a) ⊆ FP a
rw [Nat.succ_eq_one_add, ← Stream'.drop_drop]
no goals
case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop 1 (Stream'.drop n a)) ⊆ FP a
exact _root_.trans (FP.tail _) ih
no goals
case zero
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ FP (Stream'.drop Nat.zero a) ⊆ FP a
rfl