let a, b, q1, q2, r1, r2 be Element of INT.Ring ; :: thesis: ( b <> 0. INT.Ring & a = (q1 * b) + r1 & 0. INT.Ring <= r1 & r1 < abs b & a = (q2 * b) + r2 & 0. INT.Ring <= r2 & r2 < abs b implies ( q1 = q2 & r1 = r2 ) )
assume A1: ( b <> 0. INT.Ring & a = (q1 * b) + r1 & 0. INT.Ring <= r1 & r1 < abs b & a = (q2 * b) + r2 & 0. INT.Ring <= r2 & r2 < abs b ) ; :: thesis: ( q1 = q2 & r1 = r2 )
reconsider b' = b as Integer ;
reconsider q1' = q1 as Integer ;
reconsider q2' = q2 as Integer ;
reconsider r1' = r1 as Integer ;
reconsider r2' = r2 as Integer ;

now

per cases ( 0 <= r1' - r2' or r1' - r2' < 0 ) ;

case A2: 0 <= r1' - r2' ; :: thesis: q1 = q2

A3: (q2' - q1') * b' = r1' - r2' by A1;

now

per cases ( 0 = r1' - r2' or 0 <> r1' - r2' ) ;

case 0 = r1' - r2' ; :: thesis: q1 = q2

then ( q2' - q1' = 0 or b' = 0 ) by A3, XCMPLX_1:6;
hence q1 = q2 by A1, FUNCT_7:def 1; :: thesis: verum

end;

case 0 <> r1' - r2' ; :: thesis: q1 = q2

then A4: 0 <> q2' - q1' by A3;
A5: (absreal . (q2' - q1')) * (absreal . b') >= absreal . b'

proof

absreal . b' = absint . b by Def6;
then reconsider c = absreal . b' as Element of NAT ;
reconsider d' = q2' - q1' as Integer ;
reconsider e = q2 + (- q1) as Element of INT.Ring ;
absreal . d' = absint . e by Def6;
then reconsider d = absreal . d' as Element of NAT ;
d * c >= 1 * c by A4, Lm6, NAT_1:4;
hence (absreal . (q2' - q1')) * (absreal . b') >= absreal . b' ; :: thesis: verum

end;

consider i1, i2 being Integer such that
A6: ( i1 = 0. INT.Ring & i2 = r2 & i1 <= i2 ) by A1;
- r2' <= - 0 by A6, Lm3;
then A7: r1' + (- r2') <= r1' + 0 by XREAL_1:8;
A8: abs b = absint . b by Th1
.= absreal . b by Def6 ;
r1' - r2' = abs ((q2' - q1') * b') by A1, A2, ABSVALUE:def 1
.= (abs (q2' - q1')) * (abs b') by COMPLEX1:151
.= (absreal . (q2' - q1')) * (abs b') by EUCLID:def 2
.= (absreal . (q2' - q1')) * (absreal . b') by EUCLID:def 2 ;
hence q1 = q2 by A1, A5, A7, A8, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence q1 = q2 ; :: thesis: verum

end;

case A9: r1' - r2' < 0 ; :: thesis: q1 = q2

then A10: - (r1' - r2') > 0 by XREAL_1:60;
A11: - (r1' - r2') = r2' - r1' ;
(q1' - q2') * b' = r2' - r1' by A1;
then A12: 0 <> q1' - q2' by A9, A11, XREAL_1:60;
A13: (absreal . (q1' - q2')) * (absreal . b') >= absreal . b'

proof

absreal . b' = absint . b by Def6;
then reconsider c = absreal . b' as Element of NAT ;
reconsider d' = q1' - q2' as Integer ;
reconsider e = q1 + (- q2) as Element of INT.Ring ;
absreal . d' = absint . e by Def6;
then reconsider d = absreal . d' as Element of NAT ;
d * c >= 1 * c by A12, Lm6, NAT_1:4;
hence (absreal . (q1' - q2')) * (absreal . b') >= absreal . b' ; :: thesis: verum

end;

consider i1, i2 being Integer such that
A14: ( i1 = 0. INT.Ring & i2 = r1 & i1 <= i2 ) by A1;
- r1' <= - 0 by A14, Lm3;
then A15: r2' + (- r1') <= r2' + 0 by XREAL_1:8;
A16: abs b = absint . b by Th1
.= absreal . b by Def6 ;
r2' - r1' = abs ((q1' - q2') * b') by A1, A10, ABSVALUE:def 1
.= (abs (q1' - q2')) * (abs b') by COMPLEX1:151
.= (absreal . (q1' - q2')) * (abs b') by EUCLID:def 2
.= (absreal . (q1' - q2')) * (absreal . b') by EUCLID:def 2 ;
hence q1 = q2 by A1, A13, A15, A16, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence ( q1 = q2 & r1 = r2 ) by A1; :: thesis: verum