Theorem Stream'.Seq.at_least_as_long_as_coind

Modification history

2025-09-17 05:19
Mathlib/Data/Seq/Basic.lean
feat(Data/Seq): coinductive predicates for sequences (#28874) …
Added Stream'.Seq.at_least_as_long_as_coindView on Github →