feat: in a C⋆-algebra, if 1 ≤ a, then a ^ · is monotone (#18351)

feat: in a C⋆-algebra, if 1 ≤ a, then a ^ · is monotone (#18351) #11505