fix(order/sub): make arguments explicit (#9541)
* This makes some arguments of lemmas explicit.
* These lemmas were not used in places where the implicitness/explicitness of the arguments matters
* Providing the arguments is sometimes useful, especially in `rw ← ...`
* This follows the explicitness of similar lemmas (like the instantiations for `nat`).
Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
