a |-count ((a |^ b) * (- 1)) = b + (a |-count (- 1)) by NEWTON03:105;
hence a |-count (- (a |^ b)) = b ; :: thesis: verum