for a, b being non zero non unit Real holds (op1 a) / (op1 b) = b / a ;