feat: in a C⋆-algebra, b⁻¹ ≤ a⁻¹ ↔ a ≤ b for nonnegative a b : Aˣ (#16364)

b⁻¹ ≤ a⁻¹ ↔ a ≤ b

a b : Aˣ