feat: semiring `*` propagators in `grind`

This PR adds propagation rules corresponding to `Semiring`
normalization rules added at #11628. The new rules are only for
non-commutative semirings because they have limited support in
`grind`, and the new normalization rules created surprises in Mathlib
because they neutralize parameters such as `one_mul`. Any theorem instance
associated with this parameter is reduced to `True` by the normalizer.