(((a * b) + 1) |^ n) mod b = ((((a * b) + 1) mod b) |^ n) mod b by GR_CY_3:30
.= 1 ;
hence (((a * b) + 1) |^ n) mod b = 1 ; :: thesis: verum