feat(data/nat/prime): factors sublist of product (#11104)
feat(data/nat/prime): factors sublist of product (#11104)

This PR changes the existing `factors_subset_right` to give a stronger sublist conclusion (which trivially can be used to reproduce the subst version).





leanprover-community/mathlib,leanprover-community/mathlib