mathlib3

fbebf1a0 - chore(algebra/order/ring): golf a few proofs (#16398)