theorem shreq0 (a b: nat): $ shr a b = 0 <-> a < 2 ^ b $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | diveq0 | 2 ^ b != 0 -> (a // 2 ^ b = 0 <-> a < 2 ^ b) |
|
2 | 1 | conv shr | 2 ^ b != 0 -> (shr a b = 0 <-> a < 2 ^ b) |
3 | pow2ne0 | 2 ^ b != 0 |
|
4 | 2, 3 | ax_mp | shr a b = 0 <-> a < 2 ^ b |