reconsider b' = b as Integer ;

now

per cases ( 0 <= b' or b' < 0 ) ;

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

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

end;

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

then A3: 0 < - b' by XREAL_1:60;
reconsider c = - b' as Element of INT.Ring by INT_1:def 2;
consider q, r being Element of INT.Ring such that
A4: ( a = (q * c) + r & 0. INT.Ring <= r & r < abs c ) by A3, Lm3, Lm8;
reconsider t = - q as Element of INT.Ring ;
A5: (t * b) + r = a by A4;
( 0. INT.Ring <= r & r < abs b )

proof

absint . c = absreal . c by Def6
.= abs (- b') by EUCLID:def 2
.= - b' by A3, ABSVALUE:def 1
.= abs b' by A2, ABSVALUE:def 1
.= absreal . b' by EUCLID:def 2
.= absint . b by Def6
.= abs b by Th1 ;
hence ( 0. INT.Ring <= r & r < abs b ) by A4, Th1; :: thesis: verum

end;

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

end;

end;

end;

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