let r be Nat; :: thesis: ( r = k div l iff ( ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) )

per cases ( l = 0 or l > 0 ) ;

suppose l = 0 ; :: thesis: ( r = k div l iff ( ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) )

hence ( r = k div l iff ( ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) ) ; :: thesis: verum

end;

suppose A1: l > 0 ; :: thesis: ( r = k div l iff ( ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) )

then A2: k = (l * (k div l)) + (k mod l) by INT_1:59;
A3: k mod l is Nat by Lm2;
hence ( not r = k div l or ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) by A1, A2, INT_1:58; :: thesis: ( ( ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) implies r = k div l )
assume A4: ( ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) ; :: thesis: r = k div l
A5: k mod l < l by A1, INT_1:58;
k div l is Nat by Lm1;
hence r = k div l by A2, A3, A4, A5, NAT_1:18; :: thesis: verum

end;

end;