take absint ; :: according to INT_3:def 8 :: thesis: for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )
let a, b be Element of INT.Ring; :: thesis: ( b <> 0. INT.Ring implies ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) )
reconsider b9 = b as Integer ;
assume A1: b <> 0. INT.Ring ; :: thesis: ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )

now

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

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

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

end;

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

reconsider c = - b9 as Element of INT.Ring ;
0 < - b9 by A2, XREAL_1:58;
then consider q, r being Element of INT.Ring such that
A3: a = (q * c) + r and
A4: ( r = 0. INT.Ring or absint . r < absint . c ) by Lm3, Lm6;
A5: ( r = 0. INT.Ring or absint . r < absint . b )

proof

assume A6: r <> 0. INT.Ring ; :: thesis: absint . r < absint . b
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 ;
hence absint . r < absint . b by A4, A6; :: thesis: verum

end;

reconsider t = - q as Element of INT.Ring ;
(t * b) + r = a by A3;
hence ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) by A5; :: thesis: verum

end;

end;

end;

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