reconsider m = n / 2 as Nat ;
((b - 1) |^ (2 * m)) mod b = (((b - 1) |^ 2) |^ m) mod b by NEWTON:9
.= (((b - 1) * (b - 1)) |^ m) mod b by NEWTON:81
.= (((b * (b - 2)) + 1) |^ m) mod b
.= 1 ;
hence ((b - 1) |^ n) mod b = 1 ; :: thesis: verum