feat(algebra/module/ordered): simple `smul` lemmas (#9077)
These are the negative versions of the lemmas in `ordered_smul`, which suggests that both files should be merged.
Note however that, contrary to those, they need `module k M` instead of merely `smul_with_zero k M`.
