https://github.com/math-comp/analysis/blob/8d9538acc348d7079d2b5b3abc8c68992a327893/classical/filter.v#L24 see [#math-comp analysis > nbhs ?](https://rocq-prover.zulipchat.com/#narrow/channel/237666-math-comp-analysis/topic/nbhs.20.3F/with/612391585)
analysis/classical/filter.v
Line 24 in 8d9538a
see #math-comp analysis > nbhs ?