feat(data/matrix/rank): rank of multiplication (#18784)
This adds a universe-polymorphic version of `rank_comp_le_right`, and then uses it to show `(A ⬝ B).rank ≤ B.rank`; previously we only had `(A ⬝ B).rank ≤ A.rank`.
For convenience, this adds the spellings `(A ⬝ B).rank ≤ min A.rank B.rank` and `rank (f.comp g) ≤ min (rank f) (rank g)`, as these map well to the way that rank would be described in words.
