theorem boolle1 (n: nat): $ bool n <-> n <= 1 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bicom | (n <= 1 <-> bool n) -> (bool n <-> n <= 1) |
|
2 | leltsuc | n <= 1 <-> n < suc 1 |
|
3 | 2 | conv bool, d2 | n <= 1 <-> bool n |
4 | 1, 3 | ax_mp | bool n <-> n <= 1 |