take absint ; :: according to INT_3:def 9 :: 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 ) ) )
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 ) )
reconsider b' = b as Integer ;

now

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

case 0 <= b' ; :: 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, Lm7; :: thesis: verum

end;

case A2: b' < 0 ; :: thesis: ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . 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 & ( r = 0. INT.Ring or absint . r < absint . c ) ) by A3, Lm3, Lm7;
reconsider t = - q as Element of INT.Ring ;
A5: (t * b) + r = a by A4;
( 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 (- 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 ;
hence absint . r < absint . b by A4, A6; :: thesis: verum

end;

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