reconsider m = n - 1 as even Nat ;
((b - 1) |^ (m + 1)) mod b = ((b - 1) * ((b - 1) |^ m)) mod b by NEWTON:6
.= (((b - 1) mod b) * (((b - 1) |^ m) mod b)) mod b by NAT_D:67
.= (b - 1) mod ((b - 1) + 1) ;
hence ((b - 1) |^ n) mod b = b - 1 ; :: thesis: verum