theorem zsubneg2 (a b: nat): $ a -Z -uZ b = a +Z b $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zaddeq2 | -uZ -uZ b = b -> a +Z -uZ -uZ b = a +Z b |
|
2 | 1 | conv zsub | -uZ -uZ b = b -> a -Z -uZ b = a +Z b |
3 | znegneg | -uZ -uZ b = b |
|
4 | 2, 3 | ax_mp | a -Z -uZ b = a +Z b |