let a, b, n be Nat; :: thesis: a mod (b |^ n) <= a mod (b |^ (n + 1))

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

suppose b = 0 ; :: thesis: a mod (b |^ n) <= a mod (b |^ (n + 1))

then reconsider b = b as zero Nat ;

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

suppose n = 0 ; :: thesis: a mod (b |^ n) <= a mod (b |^ (n + 1))

a mod (b |^ n) = a mod 1 ;
hence a mod (b |^ n) <= a mod (b |^ (n + 1)) ; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: a mod (b |^ n) <= a mod (b |^ (n + 1))

a mod (b |^ n) = a mod 0 ;
hence a mod (b |^ n) <= a mod (b |^ (n + 1)) ; :: thesis: verum

end;

end;

end;

suppose b > 0 ; :: thesis: a mod (b |^ n) <= a mod (b |^ (n + 1))

then b >= 1 by NAT_1:14;

per cases then ( b = 1 or b > 1 ) by XXREAL_0:1;

suppose b = 1 ; :: thesis: a mod (b |^ n) <= a mod (b |^ (n + 1))

hence a mod (b |^ n) <= a mod (b |^ (n + 1)) ; :: thesis: verum

end;

suppose b > 1 ; :: thesis: a mod (b |^ n) <= a mod (b |^ (n + 1))

then reconsider b = b as non trivial Nat by NEWTON03:def 1;
assume A1: not a mod (b |^ n) <= a mod (b |^ (n + 1)) ; :: thesis: contradiction
a mod (b |^ n) < b |^ n by NAT_D:1;
then a mod (b |^ (n + 1)) < b |^ n by A1, XXREAL_0:2;
then (a mod (b |^ n)) mod (b |^ n) > (a mod (b |^ (n + 1))) mod (b |^ n) by A1, NAT_D:24;
then (a mod (b |^ n)) mod (b |^ n) > (a mod (b * (b |^ n))) mod (b |^ n) by NEWTON:6;
hence contradiction by RADIX_1:3; :: thesis: verum

end;

end;

end;

end;