theorem sub01 (a: nat): $ 0 - a = 0 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | le02 | a <= 0 <-> a = 0 |
|
2 | sub02 | 0 - 0 = 0 |
|
3 | subeq2 | a = 0 -> 0 - a = 0 - 0 |
|
4 | 2, 3 | syl6eq | a = 0 -> 0 - a = 0 |
5 | 1, 4 | sylbi | a <= 0 -> 0 - a = 0 |
6 | nlesubeq0 | ~a <= 0 -> 0 - a = 0 |
|
7 | 5, 6 | cases | 0 - a = 0 |