English
For i < j, the product of the i-th and j-th elements lies in FP a: a.get i * a.get j ∈ FP a.
Русский
Для i < j произведение i-го и j-го элементов лежит в FP a: a.get i * a.get j ∈ FP a.
LaTeX
$$$$ \forall {M} [Semigroup M] (a : Stream' M) (i j : \mathbb{N}) (ij : i < j), a.get i * a.get j \in FP a $$$$
Lean4
@[to_additive]
theorem mul_two {M} [Semigroup M] (a : Stream' M) (i j : ℕ) (ij : i < j) : a.get i * a.get j ∈ FP a :=
by
refine FP_drop_subset_FP _ i ?_
rw [← Stream'.head_drop]
apply FP.cons
rcases Nat.exists_eq_add_of_le (Nat.succ_le_of_lt ij) with ⟨d, hd⟩
have := FP.singleton (a.drop i).tail d
rw [Stream'.tail_eq_drop, Stream'.get_drop, Stream'.get_drop] at this
convert this
cutsat
