theorem lt12 (a: nat): $ a < 1 <-> a = 0 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr3 | (a <= 0 <-> a < 1) -> (a <= 0 <-> a = 0) -> (a < 1 <-> a = 0) |
|
2 | leltsuc | a <= 0 <-> a < suc 0 |
|
3 | 2 | conv d1 | a <= 0 <-> a < 1 |
4 | 1, 3 | ax_mp | (a <= 0 <-> a = 0) -> (a < 1 <-> a = 0) |
5 | le02 | a <= 0 <-> a = 0 |
|
6 | 4, 5 | ax_mp | a < 1 <-> a = 0 |