for a, b being Real st 0 <= a & a <= b holds
a / b <= 1 by Lm37;