let m, n be Nat; :: thesis: (m mod n) mod n = m mod n

per cases ( n <> 0 or n = 0 ) ;

suppose n <> 0 ; :: thesis: (m mod n) mod n = m mod n

then ex t being Nat st
( m = (n * t) + (m mod n) & m mod n < n ) by NAT_D:def 2;
hence (m mod n) mod n = m mod n by NAT_D:24; :: thesis: verum

end;

suppose A1: n = 0 ; :: thesis: (m mod n) mod n = m mod n

hence (m mod n) mod n = 0 by NAT_D:def 2
.= m mod n by A1, NAT_D:def 2 ;
:: thesis: verum

end;

end;