let a be non zero Integer; :: thesis: for b being Integer holds
( a divides b iff a divides b mod a )
let b be Integer; :: thesis: ( a divides b iff a divides b mod a )
A1: ( a divides b implies a divides b mod a )

proof

assume a divides b ; :: thesis: a divides b mod a
then b mod a = 0 by INT162;
hence a divides b mod a by INT_2:12; :: thesis: verum

end;

( a divides b mod a implies a divides b )

proof

assume B1: a divides b mod a ; :: thesis: a divides b

per cases ( b is zero or not b is zero ) ;

suppose b is zero ; :: thesis: a divides b

hence a divides b by INT_2:12; :: thesis: verum

end;

suppose not b is zero ; :: thesis: a divides b

then reconsider b = b as non zero Integer ;
|.(b mod a).| < |.a.| by PELLS_EQ:2;
then b mod a = 0 by B1, INT_4:6;
hence a divides b by INT162; :: thesis: verum

end;

end;

end;

hence ( a divides b iff a divides b mod a ) by A1; :: thesis: verum