for a, b being positive Real st a <> b holds
ex n, m being Real st
( a = (a / b) to_power n & b = (a / b) to_power m )