>>280
つまり、最初に「÷」について、「ab＜÷(ab^{-1})」を満たすように定義すれば、
乗法・の論理的扱いとしては問題なくなる(と思うが)。