for a, b, q1, q2, r1, r2 being Element of INT.Ring st b <> 0. INT.Ring & a = (q1 * b) + r1 & 0. INT.Ring <= r1 & r1 < |.b.| & a = (q2 * b) + r2 & 0. INT.Ring <= r2 & r2 < |.b.| holds
( q1 = q2 & r1 = r2 )