Bundle zero-aware real-rooted interlacing sequences

[PerAlexandersson]

Summary

• add IsInterlacingSeq0NonnegRealRooted without changing the weak
  Prec0 or IsInterlacingSeq0Nonneg semantics
• provide receiver projections, sublist preservation, strict conversion after
  removing zero entries, and conversion from strict nonnegative sequences
• reuse sublist_of_realRooted_of_ne and
  filter_ne_zero_of_realRooted rather than duplicating their proofs
• migrate the ProductFamily left-zero filter helper to consume the bundle
  while preserving the public theorem signature

Scope

This is generic cleanup infrastructure for #328. It deliberately does not
encode Hoster--Stump's exceptional degree-at-most-one convention; that
source-specific relation remains in #326.

Validation

No local build was run in this continuation.

Fixes #328.