let a, b be non zero Nat; :: thesis: (a - b) mod (2 * b) = (a + b) mod (2 * b)
((a - b) + (2 * b)) mod (2 * b) = (((a - b) mod (2 * b)) + ((2 * b) mod (2 * b))) mod (2 * b) by NAT_D:66;
hence (a - b) mod (2 * b) = (a + b) mod (2 * b) ; :: thesis: verum