reconsider b9 = b as Integer ;

now

per cases ( 0 <= b9 or b9 < 0 ) ;

case 0 <= b9 ; :: thesis: ex b₁, q being Element of INT.Ring st
( a = (q * b) + b₁ & 0. INT.Ring <= b₁ & b₁ < abs b )

then ex q, r being Element of INT.Ring st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b ) by A1, Lm8;
hence ex b₁, q being Element of INT.Ring st
( a = (q * b) + b₁ & 0. INT.Ring <= b₁ & b₁ < abs b ) ; :: thesis: verum

end;

case A2: b9 < 0 ; :: thesis: ex b₁, q being Element of INT.Ring st
( a = (q * b) + b₁ & 0. INT.Ring <= b₁ & b₁ < abs b )

reconsider c = - b9 as Element of INT.Ring ;
0 < - b9 by A2, XREAL_1:60;
then consider q, r being Element of INT.Ring such that
A3: a = (q * c) + r and
A4: 0. INT.Ring <= r and
A5: r < abs c by Lm3, Lm8;
reconsider t = - q as Element of INT.Ring ;
A6: (t * b) + r = a by A3;
absint . c = absreal . c by Def6
.= abs (- b9) by EUCLID:def 2
.= - b9 by A2, ABSVALUE:def 1
.= abs b9 by A2, ABSVALUE:def 1
.= absreal . b9 by EUCLID:def 2
.= absint . b by Def6
.= abs b by Th1 ;
then r < abs b by A5, Th1;
hence ex b₁, q being Element of INT.Ring st
( a = (q * b) + b₁ & 0. INT.Ring <= b₁ & b₁ < abs b ) by A4, A6; :: thesis: verum

end;

end;

end;

hence ex b₁, q being Element of INT.Ring st
( a = (q * b) + b₁ & 0. INT.Ring <= b₁ & b₁ < abs b ) ; :: thesis: verum