|@(quotient ?? ((div n q)-(div m q)))
>distributive_times_minus >commutative_times
>(commutative_times q) cut((n/q)*q = n - (n \mod q)) [//] #H
|@(quotient ?? ((div n q)-(div m q)))
>distributive_times_minus >commutative_times
>(commutative_times q) cut((n/q)*q = n - (n \mod q)) [//] #H