Separated int_as_nat_diff library, extra pure hints no longer need ugly ltac overriding, improved spin and ticket lock allocation specs.